Design, Implementation and Application of a Framework for the Formalization of Deductive Systems

点击翻译按钮获取中文摘要

9619584 This project is a renewal of NSF Grant CCR-9303383 with the same title. Motivated by the tremendous variety of deductive systems of interest in computer science and logic, general meta-languages for their specification, often referred to as logical frameworks, have been investigated by the researcher and others. Work on the previous grant includes the design of the logical framework LF and the logic programming language Elf based on LF. Extensive case studies have confirmed the wide range of applicability of the methodology underlying LF and Elf and also pointed towards certain limitations, which this project will address. The work includes a language for modular presentation of deductive systems and meta-programs, and refinements of the framework to permit subtyping, linearity, and internal equational reasoning. The project will implement these language refinements, building on current prototypes and the core and module language implementations for LF and Elf. It will also continue to explore the use of LF and Elf and their refinements as vehicles for representing proofs of meta theorems about deductive systems; that is, their use as a meta-logical framework. A number of case studies under the previous grant indicate the feasibility of such representations, but more theoretical and implementation work remains to be done. In longer term plans, the project will increase the degree of automation of carrying out such proofs, taking advantage of the high level of abstraction of the representations and the expressive type system of LF. ***