Informatics Report Series


Report   

EDI-INF-RR-0758


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:A Dependent Type Theory with Names and Binding
Authors: Ulrich Schoepp ; Ian Stark
Date:Sep 2004
Publication Title:Proceedings of CSL 2004 (Conference for Computer Science Logic)
Publisher:Springer
Publication Type:Conference Paper Publication Status:Published
Volume No:3210 Page Nos:235-249
DOI:10.1007/b100120
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},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh