This talk describes work in progress on a form of constructive type
theory featuring the simple computational effect of generating fresh
names combined with name equality, name swapping and name
abstraction. The motivation is to try to extend the FreshML functional
programming language (or more precisely, a fragment of it with only
totally defined functions) to a dependently typed language. FreshML
provides user-friendly support for writing syntax-manipulating
programs featuring structural recursion "modulo alpha-conversion"; but
it does so using generative names. The aim is to obtain a
constructive type theory in which such programs can also express (via
a Curry-Howard style correspondence) proofs by structural induction
modulo alpha-conversion. In such a type theory terms can involve
generative names and types can depend upon terms; therefore types
involve generative names. To understand the properties of such types,
I am guided by a relatively simple model using nominal sets.