Ulrich Berger - Strong normalisation for applied lambda calculi

lmcs:2267 - Logical Methods in Computer Science, October 5, 2005, Volume 1, Issue 2 - https://doi.org/10.2168/LMCS-1(2:3)2005
Strong normalisation for applied lambda calculiArticle

Authors: Ulrich Berger ORCID

We consider the untyped lambda calculus with constructors and recursively defined constants. We construct a domain-theoretic model such that any term not denoting bottom is strongly normalising provided all its `stratified approximations' are. From this we derive a general normalisation theorem for applied typed lambda-calculi: If all constants have a total value, then all typeable terms are strongly normalising. We apply this result to extensions of Gödel's system T and system F extended by various forms of bar recursion for which strong normalisation was hitherto unknown.

Comment: 14 pages, paper acceptet at electronic journal LMCS

https://doi.org/10.2168/LMCS-1(2:3)2005
Source: arXiv.org:cs/0507007
Volume: Volume 1, Issue 2
Published on: October 5, 2005
Imported on: January 25, 2005
Keywords: Computer Science - Computer Science and Game Theory, D.1.1, F.3.2, F.3.3, F.4.1
Licence: arXiv.org - Assumed non-exclusive license to distribute

6 Documents citing this article

Share and export

Consultation statistics

This page has been seen 3173 times.
This article's PDF has been downloaded 426 times.