author | wenzelm |
Mon, 19 Jan 2015 20:39:01 +0100 | |
changeset 59409 | b7cfe12acf2e |
parent 47839 | 3c54878ed67b |
permissions | -rw-r--r-- |
15283 | 1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
2 |
||
15582 | 3 |
<html> |
1341 | 4 |
|
15582 | 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> |
|
1341 | 13 |
|
6034 | 14 |
HOLCF is the definitional extension of Church's Higher-Order Logic with |
15 |
Scott's Logic for Computable Functions that has been implemented in the |
|
16 |
theorem prover Isabelle. This results in a flexible setup for reasoning |
|
17 |
about functional programs. HOLCF supports standard domain theory (in particular |
|
18 |
fixpoint reasoning and recursive domain equations) but also coinductive |
|
19 |
arguments about lazy datatypes. |
|
15582 | 20 |
|
21 |
<p> |
|
22 |
||
6034 | 23 |
The most recent description of HOLCF is found here: |
1341 | 24 |
|
15582 | 25 |
<ul> |
47839 | 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 |
||
32 |
Descriptions of earlier versions can also be found online: |
|
33 |
||
34 |
<ul> |
|
15582 | 35 |
<li><a href="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</a> |
36 |
</ul> |
|
1341 | 37 |
|
15582 | 38 |
A 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> |
|
24567 | 42 |
Franz Regensburger.<br> |
15582 | 43 |
Dissertation Technische Universität München.<br> |
44 |
Year: 1994. |
|
45 |
</ul> |
|
1410
324aa8134639
changed predicate flat to is_flat in theory Fix.thy
regensbu
parents:
1341
diff
changeset
|
46 |
|
3279 | 47 |
A short survey is available in: |
15582 | 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> |
|
1341 | 51 |
|
15582 | 52 |
</body> |
53 |
||
54 |
</html> |