Heterogeneous development graphs and heterogeneous borrowing

Till Mossakowski

To appear at Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France, 6-14 April, 2002


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.

Server START Conference Manager
Update Time 14 Dec 2001 at 14:02:38
Maintainer fossacs02@brics.dk.
Start Conference Manager
Conference Systems