University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence | up: Our Papers |

**Revised version of Technical Report UIB 96-10
Universität Ulm, Fakultät
für Informatik, Oct. 1997**

Abstract |

We describe an encoding of major parts of domain theory and fixed-point theory in the PVS extension of the simply-typed lambda-calculus; these formalizations comprise the encoding of mathematical structures like complete partial orders (domains), domain constructions, the Knaster-Tarski fixed-point theorem for monotonic functions, and variations of fixed-point induction. Altogether, these encodings form a conservative extension of the underlying PVS logic. A major problem of embedding mathematical theories like domain theory lies in the fact that developing and working with those theories usually generates myriads of applicability and type-correctness conditions. Our approach to exploiting the PVS devices of predicate subtypes and judgements to establish many applicability conditions behind the scenes leads to a considerable reduction in the number of the conditions that actually need to be proved. We illustrate the applicability of our encodings by means of simple examples including a mechanized fixed-point induction proof in the context of relating different semantics of imperative programming constructs.

Online Copy |

Available as Postscript (217 KB) or compressed Postscript (83 KB)

BibTeX Entry |

@TechReport{BPvHR97, author = {F. Bartels and F. W. v. Henke and H. Pfeifer and H. Rue{\ss}}, title = {Mechanizing Domain Theory}, institution = {Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik}, year = {1997}, number = {96-10}, type = {Ulmer Informatik-Berichte}, note = {This is a major revision of the Technical Report UIB-96-10 with the title "Formalizing Fixed-Point Theory in PVS". The original version can still be found at \url{http://www.informatik.uni-ulm.de/ki/PVS/fixpoints.html}}, }

Dept. of AI Homepage | Research | Help | Mail to Webmaster | H. Pfeifer - Nov 4, 1997 |