Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society


Natural semantics and some of its meta-theory in Elf

Michaylov, Spiro and Pfenning, Frank

MPI-I-91-211. August 1991, 26 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
Operational semantics provide a simple, high-level and elegant
means of specifying interpreters for programming languages. In
natural semantics, a form of operational semantics, programs
are traditionally represented as first-order tree structures
and reasoned about using natural deduction-like methods.
Hannan and Miller combined these methods with higher-order
representations using $\lambda$Prolog.

In this paper we go one step further and investigate the use
of the logic programming language Elf to represent natural semantics.
Because Elf is based on the LF Logical Framework with dependent
types, it is possible to write programs that reason about their
own partial correctness. We illustrate these techniques by giving
type checking rules and operational semantics for Mini-ML,
a small functional language based on a simply typed $\lambda$-calculus
with polymorphism, constants, products, conditionals, and
recursive function definitions. We also partially internalize
proofs for some metatheoretic properties of Mini-ML,
the most difficult of which is subject reduction.
References to related material:

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-91-211.pdfMPI-I-91-211.pdf21113 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView
URL to this document:
Hide details for BibTeXBibTeX
  AUTHOR = {Michaylov, Spiro and Pfenning, Frank},
  TITLE = {Natural semantics and some of its meta-theory in Elf},
  TYPE = {Research Report},
  INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
  ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
  NUMBER = {MPI-I-91-211},
  MONTH = {August},
  YEAR = {1991},
  ISSN = {0946-011X},