Strong normalisation for applied lambda calculi
<|reference_start|>Strong normalisation for applied lambda calculi: 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\"odel's system T and system F extended by various forms of bar recursion for which strong normalisation was hitherto unknown.<|reference_end|>
@article{berger2005strong,
    title={Strong normalisation for applied lambda calculi},
    author={Ulrich Berger},
    journal={Logical Methods in Computer Science, Volume 1, Issue 2 (October 5,
  2005) lmcs:2267},
    year={2005},
    doi={10.2168/LMCS-1(2:3)2005},
    archivePrefix={arXiv},
    eprint={cs/0507007},
    primaryClass={cs.GT}
}