Berger, Ulrich
Continuous Semantics for Termination Proofs
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.
BibTeX - Entry
@InProceedings{berger:DSP:2005:130,
author = {Ulrich Berger},
title = {Continuous Semantics for Termination Proofs},
booktitle = {Spatial Representation: Discrete vs. Continuous Computational Models},
year = {2005},
editor = {Ralph Kopperman and Michael B. Smyth and Dieter Spreen and Julian Webster},
number = {04351},
series = {Dagstuhl Seminar Proceedings},
ISSN = {1862-4405},
publisher = {Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2005/130},
annote = {Keywords: Higher-order term rewriting , termination , domain theory}
}
|
Keywords: |
|
Higher-order term rewriting , termination , domain theory |
|
Seminar: |
|
04351 - Spatial Representation: Discrete vs. Continuous Computational Models
|
|
Issue date: |
|
2005 |
|
Date of publication: |
|
2005 |
2005
