webertj@15283: webertj@15283: webertj@15582: clasohm@1341: webertj@15582: webertj@15582: webertj@15582: HOLCF/README webertj@15582: webertj@15582: webertj@15582: webertj@15582: webertj@15582:

HOLCF: A higher-order version of LCF based on Isabelle/HOL

clasohm@1341: nipkow@6034: HOLCF is the definitional extension of Church's Higher-Order Logic with nipkow@6034: Scott's Logic for Computable Functions that has been implemented in the nipkow@6034: theorem prover Isabelle. This results in a flexible setup for reasoning nipkow@6034: about functional programs. HOLCF supports standard domain theory (in particular nipkow@6034: fixpoint reasoning and recursive domain equations) but also coinductive nipkow@6034: arguments about lazy datatypes. webertj@15582: webertj@15582:

webertj@15582: nipkow@6034: The most recent description of HOLCF is found here: clasohm@1341: webertj@15582:

clasohm@1341: webertj@15582: A detailed description (in German) of the entire development can be found in: webertj@15582: webertj@15582: regensbu@1410: wenzelm@3279: A short survey is available in: webertj@15582: clasohm@1341: webertj@15582: webertj@15582: webertj@15582: