http://www.dagstuhl.de/03322

August 3 – 6 , 2003, Event 03322

Klausurtagung AG "Software Systems Engineering", Univ. Duisburg-Essen

Organizers

Klaus Pohl (Universität Duisburg – Essen, DE)

For support, please contact

Heike Clemens

Documents

External Homepage

Motivation

Logical frameworks consist of formal meta-languages for the systematic representation of families of object-logics. This notion can be summarised conveniently by the slogan Framework = Meta-language + Representation Mechanism.

Perhaps the leading example is the LF logical framework due to Harper, Honsell and Plotkin, in which the meta-language is a system of first-order dependent function types and the representation mechanism is "judgements-as-types". By varying either the meta-language or the representation mechanism, different frameworks may be obtained.

The foundational study of logical frameworks takes many forms. For example, the meta-languages may be analysed syntactically, or the categorical semantics of dependently-typed languages might be used to give a semantics to those languages. One might also study the representation mechanisms, like the embedding of models of object-logics in models of the meta-language.

Applications of logical frameworks have emerged in several different areas. Examples include program correctness, eg analysis of Hoare-type logics, logic and functional programming languages. Perhaps more surprisingly, logical frameworks have been used as the basis for a variety of projects in the formalisation of fragments of mathematics. Sometimes it is necessary to develop a suitable formalism for a problem first. An example is hardware specification and verification, where suitable languages for describing and reasoning about the designs of microprocessors must be developed.

There are some other areas where the interactions have not been well-developed, even where there is strong a priori evidence for deep, and potentially exploitable, connections. Examples include Computer Algebra, where there is a need for a better developed theory of representation; Rewriting Logics, which are an alternative approach to a generic view of logics, with applications in specification, programming languages, agents and compilation; and Labelled Deductive Systems (LDSs): the notion of labelling and its use in both the theory and implementation of frameworks.

The seminar will focus on the development of frameworks based on the algebraic definition of (logical) structure. Such a development would naturally build on the existing type-theoretic analyses, the principal objective being the design of structurally more flexible frameworks, facilitating a more abstract and more sophisticated understanding of the theory of representation of object-systems in meta-systems. In consequence, we might expect clearer connections to logical theory such as Gabbay's Labelled Deductive Systems, in which the algebraic structure of models is incorporated into deductive systems, and to potential applications in computer algebra, where there is a clear need for a systematic theory of representation. This latter application would require the integration of the desired new theory with the existing technology used in implementations of type-theoretic frameworks. We hope that the seminar will stimulate wide-ranging discussions and interactions between researchers working in the logical foundations and in the applications of frameworks as well between these people and the designers of implementation tools.

Online Publications

We offer several possibilities to publish the results of your event. Please contact marc.herbstritt(at)dagstuhl.de if you are interested.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf in the library.