Meta-logical Frameworks

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

Formal deductive systems play a central role in the areas of programming languages and logics. Firstly, they are used to define languages and their semantics at a very high-level of abstraction (e.g., type systems or operational semantics). Secondly, they form the basis for the implementation of algorithms pertaining to languages (e.g., type inference or interpretation). Thirdly, they provide a common basis for the study of meta-theory of programming languages and logics (e.g., preservation of types under evaluation). Motivated by the tremendous variety of deductive systems of interest in com- puter science and logic, general meta-languages for their specification have been investigated by the author and others. These meta-languages are often referred to as logical frameworks. When they emphasis is placed meta-theoretic reasoning they have been called meta-logical frameworks. The primary objective of the proposed work is to further the theory and practice of logic-independent, computer-assisted formal reasoning and meta-reasoning. This is a renewal of the current NSF Grant CCR-9619584. Prior relevant work by the proposer and the results from the current grant include the design and im- plementation of the logic programming language Elf based on the logical framework LF, released in September 1998 under the name Twelf. Extensive case studies have confirmed the wide range of applicability of the methodology underlying Twelf and its extension to a linear type theory. The primary emphasis of the work proposed under this renewal will be applications in education and research, and the practical and theoretical issues suggested by these applications.