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.
HOLCF was introduced in
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},
}