# Department of Computer Science and Technology

Technical reports

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

Sten Agerholm

November 1994, 31 pages

DOI: 10.48456/tr-354

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

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 = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-354.pdf},
institution =  {University of Cambridge, Computer Laboratory},
doi = 	 {10.48456/tr-354},
number = 	 {UCAM-CL-TR-354}
}