DagSemProc.04351.11.pdf
- Filesize: 196 kB
- 19 pages
Document
Continuous Semantics for Termination Proofs
Author
-
Part of:
Volume:
Dagstuhl Seminar Proceedings, Volume 4351
Series: Dagstuhl Seminar Proceedings (DagSemProc) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2005-04-22
Cite As Get BibTex
Ulrich Berger. Continuous Semantics for Termination Proofs. In Spatial Representation: Discrete vs. Continuous Computational Models. Dagstuhl Seminar Proceedings, Volume 4351, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2005)
https://doi.org/10.4230/DagSemProc.04351.11
Abstract
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.
Subject Classification
Keywords
- Higher-order term rewriting
- termination
- domain theory
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads