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

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

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.