## A Dependent Type Theory with Names and Binding

Ulrich Schöpp
and Ian Stark

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.

### 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.

@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.

#### Page last modified:
Tuesday 5 August 2008