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