Strong normalisation for applied lambda calculi
arXiv:cs/0507007 · doi:10.2168/LMCS-1(2:3)2005
Abstract
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.
14 pages, paper acceptet at electronic journal LMCS