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 |