Lecture 11: Meta-Theory

The goal of this lecture is to convey the idea, that the logical framework LF is not only good for the representation of object languages, such as Mini-ML, the specification of algorithms, such as its operational semantics, or type inference, but also for the formalization of its meta-theory.

Taking the valued soundness theorem of Mini-ML as example, we explain the idea of realizability and demonstrate of how to program realizers in Twelf.

Suggested Reading Materials:

Frank Pfenning. Computation and Deduction, Chapter 3.7

Source Code:

val-sound.elf