Conference proceeding
Hereditary Substitution for the lambda Delta-Calculus
Electronic proceedings in theoretical computer science, Vol.127, pp.45-65
09/05/2013
DOI: 10.4204/EPTCS.127.4
Abstract
Hereditary substitution is a form of type-bounded iterated substitution, first made explicit byWatkins et al. and Adams in order to show normalization of proof terms for various constructive logics. This paper is the first to apply hereditary substitution to show normalization of a type theory corresponding to a non-constructive logic, namely the lambda Delta-calculus as formulated by Rehof. We show that there is a non-trivial extension of the hereditary substitution function of the simply-typed lambda-calculus to one for the lambda Delta-calculus. Then hereditary substitution is used to prove normalization.
Details
- Title: Subtitle
- Hereditary Substitution for the lambda Delta-Calculus
- Creators
- Harley Eades - University of IowaAaron Stump - University of Iowa
- Resource Type
- Conference proceeding
- Publication Details
- Electronic proceedings in theoretical computer science, Vol.127, pp.45-65
- DOI
- 10.4204/EPTCS.127.4
- ISSN
- 2075-2180
- eISSN
- 2075-2180
- Publisher
- Open Publ Assoc
- Number of pages
- 21
- Language
- English
- Date published
- 09/05/2013
- Academic Unit
- Computer Science
- Record Identifier
- 9984411062402771
Metrics
26 Record Views