Multi-Level Contextual Type Theory
Contextual type theory distinguishes between bound variables and meta-variables to write potentially incomplete terms in the presence of binders. It has found good use as a framework for concise explanations of higher-order unification, characterize holes in proofs, and in developing a foundation for programming with higher-order abstract syntax, as embodied by the programming and reasoning environment Beluga. However, to reason about these applications, the authors need to introduce meta2- variables to characterize the dependency on meta-variables and bound variables. In other words, they must go beyond a two-level system granting only bound variables and meta-variables.