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
Publisher DOI
Sponsorship
Engineering and Physical Sciences Research Council (EP/K008528/1)
Engineering and Physical Sciences Research Council (EP/H005633/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.