The workshop is broad in scope and covers the design of logical frameworks, meta-theoretical studies, comparative studies, implementation, and evaluation. It also covers all aspects of their use including techniques of representation of logics and languages, proofs of properties of languages, and proofs of correctness of programs. The overall aim of the workshop is to provide an understanding of the state-of-the-art of the field, to expose new research directions, and to increase the communication between the designers, implementors, and practitioners.

Logical frameworks and meta-languages are intended as a common substrate for implementing a wide variety of logics and formal systems. Their definition and implementation has been the focus of considerable work over the last decade. The underpinning of each framework or language that has been proposed is a general theory of inference systems that captures uniformities across different logics. These generalities can then be exploited in implementing systems such as theorem provers and those intended for proof and program development. Examples of logics that can be represented inside logical frameworks include higher-order logics for reasoning about high-level programming languages, logics of concurrency, modal logics, specification languages used in the design of large software systems, and formal systems describing languages. Logical frameworks themselves have been based on a variety of different languages including higher-order (intuitionistic) logics, theories of dependent types, linear logic, and modal logic. These choices lead to differences in strength in representing relevant formal systems, some of which have been examined in recent research. Work on logical frameworks and meta-languages has been supported by a variety of initiatives including several ESPRIT projects which held associated workshops.

Recently, there has also been a growing interest in logical frameworks in which it is possible to both specify and reason about the encoded logics. For frameworks that support higher-order abstract syntax, one particular challenge is to provide reasoning by induction. This task is complicated by the fact that the use of this syntax can lead to definitions for which there are no monotone inductive operators. The ability to define recursive functions inside this kind of framework is also of interest and presents similar challenges. In recent developments, a variety of new languages and techniques have been proposed which make progress in this direction. Alternative approaches include frameworks based on inductive definitions or some form of equational or rewriting logic in which substitution is explicitly encoded.

In addition to ongoing research on many of the foundational aspects mentioned above, there are numerous research groups working on systems that implement various logical frameworks and apply them to large case studies in a variety of domains. Examples of existing systems for which there is active ongoing work include Coq, Isabelle, lambdaProlog, and Twelf. An active area of research in such systems is the study of automated reasoning techniques. Current work includes the development of various automated procedures as well as the investigation of rewriting tools that use reflection or make use of links with systems that already have sophisticated rewriting systems. Program extraction and optimization are additional topics of ongoing work.

• LFM accepted papers
• LFM program
• Participant list for LFM

Workshop webpage with more information

Program Committee

• chair: Frank Pfenning <fp@cs.cmu.edu>, Carnegie Mellon U, USA
• David Basin, U Freiburg, Germany
• Thierry Coquand, Chalmers U of Techn., Sweden
• Amy Felty, U Ottawa, Canada
• Didier Galmiche, LORIA Nancy, France
• Dale Miller, Penn State U, USA
• Tobias Nipkow, Techn. U of Munich, Germany
• Benjamin C. Pierce, U Pennsylvania, USA
• Benjamin Werner, INRIA Rocquencourt, France

Organizer

Frank Pfenning <fp@cs.cmu.edu>, Carnegie Mellon U, USA