Hereditary Substitution for the λΔ-Calculus

Harley Eades
(University of Iowa)
Aaron Stump
(University of Iowa)

Hereditary substitution is a form of type-bounded iterated substitution, first made explicit by Watkins 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.

In Ugo de'Liguoro and Alexis Saurin: Proceedings First Workshop on Control Operators and their Semantics (COS 2013), Eindhoven, The Netherlands, June 24-25, 2013 , Electronic Proceedings in Theoretical Computer Science 127, pp. 45–65.
Published: 4th September 2013.

ArXived at: https://dx.doi.org/10.4204/EPTCS.127.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org