https://www.dagstuhl.de/03322

03. – 06. August 2003, Event 03322

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

Organisator

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

Auskunft zu diesem Event erteilt

Heike Clemens

Dokumente

Externe 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.

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von
Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact aufgelistet und separat in der Bibliothek präsentiert.