Continuous Semantics for Termination Proofs

Author Ulrich Berger



PDF
Thumbnail PDF

File

DagSemProc.04351.11.pdf
  • Filesize: 196 kB
  • 19 pages

Document Identifiers

Author Details

Ulrich Berger

Cite AsGet 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.
Keywords
  • Higher-order term rewriting
  • termination
  • domain theory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail