Name | Date | Size | ||
---|---|---|---|---|
.. | 30-Oct-2020 | 171 | ||
Adm.thy | H A D | 25-Jul-2019 | 7.2 KiB | |
Algebraic.thy | H A D | 25-Jul-2019 | 9.4 KiB | |
Bifinite.thy | H A D | 25-Jul-2019 | 10.2 KiB | |
Cfun.thy | H A D | 25-Jul-2019 | 19.1 KiB | |
Compact_Basis.thy | H A D | 25-Jul-2019 | 3.8 KiB | |
Completion.thy | H A D | 25-Jul-2019 | 15.6 KiB | |
Cont.thy | H A D | 25-Jul-2019 | 7.5 KiB | |
ConvexPD.thy | H A D | 25-Jul-2019 | 24 KiB | |
Cpodef.thy | H A D | 25-Jul-2019 | 10.1 KiB | |
Cprod.thy | H A D | 25-Jul-2019 | 1.3 KiB | |
Deflation.thy | H A D | 25-Jul-2019 | 13.9 KiB | |
Discrete.thy | H A D | 25-Jul-2019 | 767 | |
document/ | H | 25-Jul-2019 | 3 | |
Domain.thy | H A D | 25-Jul-2019 | 13.1 KiB | |
Domain_Aux.thy | H A D | 25-Jul-2019 | 12.3 KiB | |
ex/ | H | 25-Jul-2019 | 14 | |
Fix.thy | H A D | 25-Jul-2019 | 8.4 KiB | |
Fixrec.thy | H A D | 25-Jul-2019 | 8.4 KiB | |
FOCUS/ | H | 25-Jul-2019 | 8 | |
Fun_Cpo.thy | H A D | 25-Jul-2019 | 4.8 KiB | |
HOLCF.thy | H A D | 25-Jul-2019 | 247 | |
IMP/ | H | 25-Jul-2019 | 5 | |
IOA/ | H | 30-Oct-2020 | 27 | |
Library/ | H | 25-Jul-2019 | 14 | |
Lift.thy | H A D | 25-Jul-2019 | 4 KiB | |
LowerPD.thy | H A D | 25-Jul-2019 | 18.6 KiB | |
Map_Functions.thy | H A D | 25-Jul-2019 | 19.8 KiB | |
One.thy | H A D | 25-Jul-2019 | 2.3 KiB | |
Pcpo.thy | H A D | 25-Jul-2019 | 7.8 KiB | |
Porder.thy | H A D | 25-Jul-2019 | 11.4 KiB | |
Powerdomains.thy | H A D | 25-Jul-2019 | 6.9 KiB | |
Product_Cpo.thy | H A D | 25-Jul-2019 | 9.2 KiB | |
README.html | H A D | 25-Jul-2019 | 1.7 KiB | |
Representable.thy | H A D | 25-Jul-2019 | 22.4 KiB | |
Sfun.thy | H A D | 25-Jul-2019 | 2 KiB | |
Sprod.thy | H A D | 25-Jul-2019 | 7.9 KiB | |
Ssum.thy | H A D | 25-Jul-2019 | 7.7 KiB | |
Tools/ | H | 30-Oct-2020 | 9 | |
Tr.thy | H A D | 25-Jul-2019 | 5.7 KiB | |
Tutorial/ | H | 25-Jul-2019 | 6 | |
Universal.thy | H A D | 25-Jul-2019 | 31.7 KiB | |
Up.thy | H A D | 25-Jul-2019 | 8.1 KiB | |
UpperPD.thy | H A D | 25-Jul-2019 | 18.6 KiB |
README.html
1<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> 2 3<html> 4 5<head> 6 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1"> 7 <title>HOLCF/README</title> 8</head> 9 10<body> 11 12<h3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</h3> 13 14HOLCF is the definitional extension of Church's Higher-Order Logic with 15Scott's Logic for Computable Functions that has been implemented in the 16theorem prover Isabelle. This results in a flexible setup for reasoning 17about functional programs. HOLCF supports standard domain theory (in particular 18fixpoint reasoning and recursive domain equations) but also coinductive 19arguments about lazy datatypes. 20 21<p> 22 23The most recent description of HOLCF is found here: 24 25<ul> 26 <li><a href="http://web.cecs.pdx.edu/~brianh/phdthesis.html">HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs</a>, <br> 27 Brian Huffman.<br> 28 Ph.D. thesis, Portland State University.<br> 29 Year: 2012. 30</ul> 31 32Descriptions of earlier versions can also be found online: 33 34<ul> 35 <li><a href="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</a> 36</ul> 37 38A detailed description (in German) of the entire development can be found in: 39 40<ul> 41 <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf">HOLCF: eine konservative Erweiterung von HOL um LCF</a>, <br> 42 Franz Regensburger.<br> 43 Dissertation Technische Universität München.<br> 44 Year: 1994. 45</ul> 46 47A short survey is available in: 48<ul> 49 <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</a><br> 50</ul> 51 52</body> 53 54</html> 55