Continuous semantics for strong normalisation
Ulrich Berger · Mathematical Structures in Computer Science · 2006
We prove a general strong normalisation theorem for higher type rewrite systems based on Tait's strong computability predicates and a strictly continuous domain-theoretic semantics. The theorem applies to extensions of Gödel's system T, but also to various forms of barrecursion for which strong normalisation was hitherto unknown.