@inproceedings{ee3a8e2bea514494bd891ae9c1572876,
title = "A dependent type theory with names and binding",
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 N, 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 Pi* and sums Sigma*, as well as a propositions-as-types generalisation H of the freshness quantifier.",
author = "U Schopp and Ian Stark",
year = "2004",
doi = "10.1007/978-3-540-30124-0_20",
language = "English",
isbn = "978-3-540-23024-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "235--249",
editor = "J Marcinkowski and A Tarlecki",
booktitle = "Computer Science Logic",
address = "United Kingdom",
note = "18th International Workshop on Computer Science Logic/13th Annual Conference of the European-Association-for-Computer-Science-Logic ; Conference date: 20-09-2004 Through 24-09-2004",
}