Continuous Semantics for Termination Proofs
Ulrich Berger · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2005
We prove a general strong normalization 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 Goedel's system $T$, but also to various forms of bar recursion for which termination was hitherto unknown.