Development graphs are a tool for dealing with structured
specifications in a formal program development in order to ease the
management of change and reusing proofs. Often, different aspects of
a software system have to be specified in different logics, since
the construction of a huge logic covering all needed features would
be too complex to be feasible. Therefore, we introduce {\em
heterogeneous development graphs} as a means to cope with
heterogeneous specifications.
We cover both the semantics and the proof theory of heterogeneous
development graphs A proof calculus can be obtained either by
combining proof calculi for the individual logics, or by
representing these in some ``universal'' logic like higher-order
logic in a coherent way and then ``borrowing'' its calculus for the
heterogeneous language.
Last but not least, we sketch how these results can also be applied
to programming languages.
