Accession Number : ADA302983

Title :   A Computational Meta Logic for the Horn Fragment of LF.

Descriptive Note : Master's thesis,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA SCHOOL OF COMPUTER SCIENCE

Personal Author(s) : Schuermann, Carsten

PDF Url : ADA302983

Report Date : 06 DEC 1995

Pagination or Media Count : 158

Abstract : The logical framework LF is a type theory defined by Harper, Honsell and Plotkin. It is well-suited to serve as'a meta language to represent deductive systems. LF and its logic programming implementation Elf are also well-suited to represent meta-theoretic proofs and their computational content, but search for such proofs lies outside the framework. This thesis proposes a computational meta logic (MLF) for the Horn fragment of LF. The Horn fragment is a significant restriction of LF but it is powerful enough to represent non-trivial problems. This thesis demonstrates how MLF can be used for the problem of compiler verification. It also discusses some theoretical properties of MLF.

Descriptors :   *COMPUTER PROGRAMMING, COMPUTATIONS, THEORY, COMPUTER LOGIC, SEMANTICS, THESES, COMPUTER PROGRAM VERIFICATION, COMPILERS.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE