Lecture 8: The Logical Framework LF: Part II

We discuss the logical framework LF, in particular, the syntactic categories of objects, types, and kinds, signatures, contexts. Their validity is given in form of judgments and inference rules. We also present a congruence relation for convertibility on objects, types, and kinds, which is the closure of beta- and eta-conversion.

Using this congruence relation, the set of all objects, and all types can be divided into equivalence classes. Each equivalence only contains objects that are convertible to one another. Moreover, each of these equivalence classes has a unique representative which we call a canonical form, which we characterize inductively. Thus, any two objects can be easily compared for convertibility, by computing the canoncial forms and comparing them.

The main result of this lecture therefore is, that LF possesses a notion of canonical forms which are appropriate for the adequate representation of deductive systems. In fact we show that our representation of the operational semantics from the previous lecture is adequate in the sense that there is a bijection between derivations of the jugdment "e evaluates to v" and canonical LF objects M of type "eval rep(e) rep(v)".

Suggested Reading Materials:

Henk Barendregt. Lambda Calculi with Types., Handbook of Logic in Computer Science, Volume II, Oxford University Press.

Robert Harper, Furio Honsell, Gordon Plotkin. A Framework for Defining Logics, JACM, 1993.

Frank Pfenning. Computation and Deduction, Chapter 3

Previous lecture: Lecture 7
Next lecture: Lecture 9