Lecture 18: The Meta-Logic M2+ (Part II)

In this lecture we discuss the formal aspects of M2+. In particular, we introduce three different variable concepts necessary to define a derivability relation for functions in M2+: Variables of the first range over arbitrary LF objects, variables of the second range over variable blocks and variables of third over functions in M2+. We pay particular attention to the design of the operator that introduces new parameters.

We conclude the presentation with the observation that the type theory M2+ can be easily turned into a meta-logic by side conditions that enforce coverage and termination of each well-typed proof term.

Suggested Reading Materials:

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