Mechanizing Domain Theory
Revised version of
UIB-96-10 as of October 1997.
Authors
Falk Bartels and Holger Pfeifer and F.W. von Henke and Harald Rueß
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.
gzipped postscript
or
postscript
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
\ulr{http://www.informatik.uni-ulm.de/ki/PVS/fixpoints.html}},
}
PVS theories
These encodings have been adjusted to PVS version 2.3 and might
be slightly out of sync with the description above.
Harald Ruess:
ruess@csl.sri.com
