A Dependent Type Theory with Names and Binding

9 years 5 months ago
A Dependent Type Theory with Names and Binding
We consider the problem of providing formal support for working tract 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 Π∗ and sums Σ∗ , as well as a propositions-as-types generalisation H of t...
Ulrich Schöpp, Ian Stark
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CSL
Authors Ulrich Schöpp, Ian Stark
Comments (0)