A dependent type theory with names and binding

U Schopp*, Ian Stark

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publication18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004. Proceedings
EditorsJ Marcinkowski, A Tarlecki
Place of PublicationBerlin
PublisherSpringer
Pages235-249
Number of pages15
ISBN (Electronic)978-3-540-23024-3
ISBN (Print)978-3-540-23024-3
DOIs
Publication statusPublished - 2004
Event18th International Workshop on Computer Science Logic/13th Annual Conference of the European-Association-for-Computer-Science-Logic - Karpacz, Poland
Duration: 20 Sept 200424 Sept 2004

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume3210
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Workshop on Computer Science Logic/13th Annual Conference of the European-Association-for-Computer-Science-Logic
Country/TerritoryPoland
CityKarpacz
Period20/09/0424/09/04

Fingerprint

Dive into the research topics of 'A dependent type theory with names and binding'. Together they form a unique fingerprint.

Cite this