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 |
id |
fttriple:oai:gotriple.eu:10670/1.54ndkj |
---|---|
record_format |
openpolar |
spelling |
fttriple:oai:gotriple.eu:10670/1.54ndkj 2023-05-15T15:41:51+02:00 Multi-level Contextual Type Theory Boespflug, Mathieu Pientka, Brigitte 2011-10-31 https://doi.org/10.4204/EPTCS.71.3 http://arxiv.org/abs/1111.0087 en eng EPTCS 71, 2011, pp. 29-43 doi:10.4204/EPTCS.71.3 10670/1.54ndkj http://arxiv.org/abs/1111.0087 undefined arXiv psy lang Text https://vocabularies.coar-repositories.org/resource_types/c_18cf/ 2011 fttriple https://doi.org/10.4204/EPTCS.71.3 2023-01-22T18:31:33Z 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 Text Beluga Beluga* Unknown Eta ENVELOPE(-62.917,-62.917,-64.300,-64.300) Electronic Proceedings in Theoretical Computer Science 71 29 43 |
institution |
Open Polar |
collection |
Unknown |
op_collection_id |
fttriple |
language |
English |
topic |
psy lang |
spellingShingle |
psy lang Boespflug, Mathieu Pientka, Brigitte Multi-level Contextual Type Theory |
topic_facet |
psy lang |
description |
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 |
format |
Text |
author |
Boespflug, Mathieu Pientka, Brigitte |
author_facet |
Boespflug, Mathieu Pientka, Brigitte |
author_sort |
Boespflug, Mathieu |
title |
Multi-level Contextual Type Theory |
title_short |
Multi-level Contextual Type Theory |
title_full |
Multi-level Contextual Type Theory |
title_fullStr |
Multi-level Contextual Type Theory |
title_full_unstemmed |
Multi-level Contextual Type Theory |
title_sort |
multi-level contextual type theory |
publishDate |
2011 |
url |
https://doi.org/10.4204/EPTCS.71.3 http://arxiv.org/abs/1111.0087 |
long_lat |
ENVELOPE(-62.917,-62.917,-64.300,-64.300) |
geographic |
Eta |
geographic_facet |
Eta |
genre |
Beluga Beluga* |
genre_facet |
Beluga Beluga* |
op_source |
arXiv |
op_relation |
EPTCS 71, 2011, pp. 29-43 doi:10.4204/EPTCS.71.3 10670/1.54ndkj http://arxiv.org/abs/1111.0087 |
op_rights |
undefined |
op_doi |
https://doi.org/10.4204/EPTCS.71.3 |
container_title |
Electronic Proceedings in Theoretical Computer Science |
container_volume |
71 |
container_start_page |
29 |
op_container_end_page |
43 |
_version_ |
1766374735817474048 |