A Computational Meta Logic for the Horn Fragment of LF.

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 06, 1995
Accession Number
ADA302983

Entities

People

  • Carsten Schuermann

Organizations

  • Carnegie Mellon University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Artificial Intelligence
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Instruction Set Architecture
  • Instructions
  • Judgment
  • Language
  • Notation
  • Programming Languages
  • Reasoning
  • Standards
  • Theoretical Computer Science

Fields of Study

  • Computer science

Readers

  • Computational Linguistics