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.

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 = 	 {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}
}