TITLE: Design, Implementation, & Application of a Framework Formal deductive systems play a central role in the areas of programming languages and logics. First, they are used to define languages and their semantics at a very high-level of abstraction (e.g., type systems or operational semantics). Second, they form the basis for the implementation of algorithms pertaining to languages (e.g., type inference or interpretation). Third, 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 computer science and logic, general meta-languages for their specification have been investigated. These meta-languages are often referred to as logical frameworks. The objective of this effort is to further the theory and practice of logic-independent, computer-assisted formal reasoning and meta-reasoning. This research addresses definitional, operational, and meta-theoretical aspects of logical frameworks comprising work on further design, implementation, and application of such frameworks.

Agency
National Science Foundation (NSF)
Institute
Division of Computer and Communication Foundations (CCF)
Application #
9303383
Program Officer
D. Helen Gill
Project Start
Project End
Budget Start
1993-09-01
Budget End
1997-02-28
Support Year
Fiscal Year
1993
Total Cost
$388,159
Indirect Cost
Name
Carnegie-Mellon University
Department
Type
DUNS #
City
Pittsburgh
State
PA
Country
United States
Zip Code
15213