A Dependent Type Theory with Abstractable Names
This paper describes a version of Martin-Löf's dependent type
theory extended with names and constructs for freshness and
name-abstraction derived from the theory of nominal sets. We aim for
a type theory for computing and proving (via a Curry-Howard
correspondence) with syntactic structures which captures familiar,
but informal, "nameful" practices when dealing with binders.