In Computer Science Logic: Proceedings of the 18th International Workshop CSL 2004, Karpacz, Poland, September 20–24, 2004, Lecture Notes in Computer Science 3210, pages 235–249. Springer-Verlag, 2004.
Fetch paper (PDF, 215k). Go to other papers, talks or home page.
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.
@InProceedings{schoepp/stark:names+binding,
author = {Ulrich {Sch\"opp} and Ian Stark},
title = {A Dependent Type Theory with Names and Binding},
booktitle = {Computer Science Logic: Proceedings of the 18th
International Workshop CSL~2004},
pages = {235--249},
year = 2004,
number = 3210,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
url = {http://www.inf.ed.ac.uk/~stark/names+binding.html},
pdf = {http://www.inf.ed.ac.uk/~stark/names+binding.pdf}
}
This research was supported by the EPSRC project GR/R04430/01 Reasoning with Names and Identity in Programming Languages.