PLS Lab

Higher-order logic of Computable Functions (HOLCF)

The higher-order logic of computable functions, or HOLCF, is an extension of LCF with the reasoning facilities of higher-order logic.

HOLCF was first introduced by F. Regensburger in his 1994 thesis at TMU, with the first presentation being Regensburger 1995.

HOLCF is implemented in Isabelle, as Isabelle/HOLCF.

References

Regensburger, Franz. ‘HOLCF: Higher Order Logic of Computable Functions’. In Higher Order Logic Theorem Proving and Its Applications, edited by E. Thomas Schubert and James Alves-Foss, 971:293–307. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg, 1995. https://doi.org/10.1007/3-540-60275-5_72. 
@incollection{regensburger_1995,
	address = {Berlin, Heidelberg},
	title = {{HOLCF}: {Higher} order logic of computable functions},
	volume = {971},
	booktitle = {Higher {Order} {Logic} {Theorem} {Proving} and {Its} {Applications}},
	publisher = {Springer Berlin Heidelberg},
	author = {Regensburger, Franz},
	editor = {Thomas Schubert, E. and Alves-Foss, James},
	year = {1995},
	doi = {10.1007/3-540-60275-5_72},
	series = {Lecture Notes in Computer Science},
	pages = {293--307},
}
Müller, Olaf, Tobias Nipkow, David Von Oheimb, and Oscar Slotosch. ‘HOLCF = HOL + LCF’. Journal of Functional Programming 9, no. 2 (1999): 191–223. https://doi.org/10.1017/S095679689900341X. 
@article{muller_1999,
	title = {{HOLCF} = {HOL} + {LCF}},
	volume = {9},
	doi = {10.1017/S095679689900341X},
	number = {2},
	journal = {Journal of Functional Programming},
	author = {M\"{u}ller, Olaf and Nipkow, Tobias and Von Oheimb, David and Slotosch, Oscar},
	year = {1999},
	pages = {191--223},
}