Author
Sten Agerholm
Abstract
Most new theorem provers implement strong and complicated type
theories which eliminate some of the limitations of simple type
theories such as the HOL logic. A more accessible alternative might be
to use a combination of set theory and simple type theory as in HOL-ST
which is a version of the HOL system supporting a ZF-like set theory
in addition to higher order logic. This paper presents a case study on
the use of HOL-ST to build a model of the
-calculus by
formalising the inverse limit construction of domain theory. This
construction is not possible in the HOL system itself, or in simple
type theories in general.