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

Formalizing Fixed-Point Theory in PVS

F. Bartels, A. Dold, F.W. v. Henke, H. Pfeifer, H. Rueß

Technical Report UIB 96-10, Universität Ulm, Fakultät für Informatik, Dec. 1996


 Abstract

We describe an encoding of major parts of domain theory in the PVS extension of the simply-typed lambda-calculus; these encodings consist of:

Altogether, these encodings form a conservative extension of the underlying PVS logic, since all developments are purely definitional. Most of our proofs are straightforward transcriptions of textbook knowledge. The purpose of this work, however, was not to merely reproduce textbook knowledge. To the contrary, our main motivation derived from our work on fully mechanized compiler correctness proofs, which requires a full treatment of fixed-point induction in PVS; these requirements guided our selection of which elements of domain theory were formalized.

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 device of 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.

Finally, we exemplify the application of mechanized fixed-point induction in PVS by a mechanized proof in the context of relating different semantics of imperative programming constructs.

 Online Copy

Available as Postscript (352 KB) or compressed Postscript (132 KB)

PVS specification files: fixpoints.dmp or compressed fixpoints.dmp.gz.

To unpack the theories type M-x undump-pvs-files in PVS. The top-level theory is all_theories.pvs.

 BibTeX Entry
@TechReport{BDvH+96,
  author = "F. Bartels and A. Dold and F. W. v. Henke and H. Pfeifer and H. Rue{\ss}",
  title = "{Formalizing Fixed-Point Theory in PVS}",
  institution =  "Universit{\"a}t Ulm, Fakult{\"a}t f{\"u}r Informatik",
  year =         "1996",
  number =       "96-10",
  type = "Ulmer Informatik-Berichte"
}


Dept. of AI Homepage Research Help Mail to Webmaster H. Pfeifer - Mar. 3, 1997