- Abstract:
-
We consider the problem of providing formal support for working with abstract syntax involving variable binders. Gabbay and Pitts have shown in their work on Fraenkel-Mostowski (FM) set theory how to address this through first-class names: in this paper we present a dependent type theory for programming and reasoning with such names. Our development is based on a categorical axiomatisation of names, with freshness as its central notion. An associated adjunction captures constructions known from FM theory: the freshness quantifier И, name-binding, and unique choice of fresh names. The Schanuel topos the category underlying FM set theory is an instance of this axiomatisation. Working from the categorical structure, we define a dependent type theory which it models. This uses bunches to integrate the monoidal structure corresponding to freshness, from which we define novel multiplicative dependent products Π* and sums Σ* as well as a propositions-as-types generalisation H of the freshness quantifier.
- Copyright:
- Springer-Verlag Berlin Heidelberg 2004
- Links To Paper
- Page by author
- Page by publisher
- Bibtex format
- @InProceedings{EDI-INF-RR-0758,
- author = {
Ulrich Schoepp
and Ian Stark
},
- title = {A Dependent Type Theory with Names and Binding},
- book title = {Proceedings of CSL 2004 (Conference for Computer Science Logic)},
- publisher = {Springer},
- year = 2004,
- month = {Sep},
- volume = {3210},
- pages = {235-249},
- doi = {10.1007/b100120},
- url = {http://www.inf.ed.ac.uk/~stark/names+binding.html},
- }
|
