Repository logo
 

A Dependent Type Theory with Abstractable Names


Change log

Authors

Pitts, AM 
Matthiesen, J 
Derikx, J 

Abstract

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.

Description

Keywords

4613 Theory Of Computation, 46 Information and Computing Sciences

Journal Title

Electronic Notes in Theoretical Computer Science

Conference Name

Journal ISSN

1571-0661

Volume Title

312

Publisher

Elsevier BV
Sponsorship
Engineering and Physical Sciences Research Council (EP/K008528/1)
Engineering and Physical Sciences Research Council (EP/H005633/1)
Partially supported by the UK EPSRC program grant EP/K008528/1, Rigorous Engineering for Mainstream Systems (REMS). Supported by the UK EPSRC leadership fellowship (Peter Sewell) grant EP/H005633/1, Semantic Foundations for Real-World Systems.