Continuous Semantics for Termination Proofs
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.