The normalization problem for typed lambda calculus. Normalization by evaluation (NBE) and type-directed partial evaluation (TDPE). The completeness problem in logic: adequacy of the formal system for proving all true statements. Semantics for classical logic (Tarski's semantics). Godel's Completeness Theorem. Modifying classical semantics to intuitionistic ones: Kripke models. Catarina Coquand's link between Soundness/Completeness and NBE. Full formalization of an NBE proof in Agda for the simply typed lambda calculus. Reading material corresponding to the lectures:
Homework: Modify soundness and reify/reflect from Day2.agda below, to include conjunction (i.e. a pair type). You will need to extend the language of formulas, extend the natural deduction system with introduction and elimination rules for conjunction, and correspondingly any lemma that is proved by induction on the formula or by induction on the derivation. |