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 fo...
| Published in: | Electronic Proceedings in Theoretical Computer Science |
|---|---|
| Main Authors: | , |
| Format: | Text |
| Language: | English |
| Published: |
2011
|
| Subjects: | |
| Online Access: | https://doi.org/10.4204/EPTCS.71.3 http://arxiv.org/abs/1111.0087 |
| Summary: | 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, we need to introduce meta^2-variables to characterize the dependency on meta-variables and bound variables. In other words, we must go beyond a two-level system granting only bound variables and meta-variables. In this paper we generalize contextual type theory to n levels for arbitrary n, so as to obtain a formal system offering bound variables, meta-variables and so on all the way to meta^n-variables. We obtain a uniform account by collapsing all these different kinds of variables into a single notion of variabe indexed by some level k. We give a decidable bi-directional type system which characterizes beta-eta-normal forms together with a generalized substitution operation. Comment: In Proceedings LFMTP 2011, arXiv:1110.6685 |
|---|