Lecture 7: The Logical Framework LF: Part I

The simply typed lambda calculus is an adequate representation language for the syntactic class of expressions, but it is not adequate for representing more complex deductive systems such as, for example, the operational semantics for Mini-ML or its typing relation.

In this lecture we motivate how one goes about representing the operational semantics of Mini-ML in the dependently typed logical framework LF.

Suggested Reading Materials:

Frank Pfenning. Computation and Deduction, Chapter 3

Previous lecture: Lecture 6
Next lecture: Lecture 8