Technical reports

# Formalising a model of the λ-calculus in HOL-ST

**Sten Agerholm**

November 1994, 31 pages

## Abstract

Many 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.

## Full text

PDF (1.5 MB)

## BibTeX record

@TechReport{UCAM-CL-TR-354, author = {Agerholm, Sten}, title = {{Formalising a model of the $\lambda$-calculus in HOL-ST}}, year = 1994, month = nov, url = {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-354.pdf}, institution = {University of Cambridge, Computer Laboratory}, number = {UCAM-CL-TR-354} }