Natural Semantics and Some of Its Meta-Theory in Elf

11 years 5 months ago
Natural Semantics and Some of Its Meta-Theory in Elf
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 λ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 λ-calculus with polymorphism, constants, products, conditionals, and recursive function definitions. We also partially internalize proofs for some meta-theoretic pr...
Spiro Michaylov, Frank Pfenning
Added 27 Aug 2010
Updated 27 Aug 2010
Type Conference
Year 1991
Where ELP
Authors Spiro Michaylov, Frank Pfenning
Comments (0)