Lecture 17: The Meta-Logic M2+ (Part I)

In this lecture we motivate the meta type theory M2+. M2+ is a type system whose function range over higher-order, dependently typed functions. We show how these proofs can be used to formalize the computational content of theorems already discussed in this lecture, in particular a function that converts natural deduction derivations into sequent derivations.

We will try to give the intuition behind the regular world assumptions, and discuss strenghtening lemmas and subordination relations.

Suggested Reading Materials:

Carsten Schürmann. Programming with higher-order encodings.