Authors: Ulrich Schoepp, Ian Stark
Title: A Dependent Type Theory with Names and Binding
Abstract: 
This talk is about how names and binding can be integrated
in dependent type theory. Names and name-binding are
standard tools for working informally with abstract syntax
and variables binding.  Gabbay and Pitts have shown that
Fraenkel Mostowski (FM) set theory supports a formal notion
of names using which informal work with names and binding
can be made precise. Based on the notion of name-swapping,
Gabbay and Pitts give a number of useful constructions for
working with names, such as a syntax-independent notion of
freshness that formalises when two objects do not share
names and a freshness quantifier that simplifies work
with names.

To make FM-style name constructs suitable for integration
in dependent type theory, we give an alternative
presentation of them based on freshness rather than
swapping. This presentation has as its central primitive
a monoidal structure capturing freshness.  In analogy to
the definition of simple dependent products (Pi) and sums
(Sigma) for a cartesian structure, we define monoidal
dependent products (Pi*) and sums (Sigma*) for the monoidal
structure. We express FM constructs for names and binding,
such as alpha-equivalence classes, unique choice of fresh
names and the freshness quantifier in terms of these
dependent monoidal products and sums.

We use bunches to combine dependent types with the monoidal
structure, Pi* and Sigma*. The resulting bunched type
theory is related to the simply typed alphalambda-calculus
of O'Hearn and Pym. In addition to Pi* and Sigma*, the
type theory also features hidden-name types which are
in propositions-as-types correspondence to the freshness
quantifier.