author | huffman |
Wed, 02 Mar 2005 22:57:08 +0100 | |
changeset 15563 | 9e125b675253 |
parent 15283 | f21466450330 |
child 15582 | 7219facb3fd0 |
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 |
||
3279 | 3 |
<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY> |
1341 | 4 |
|
3279 | 5 |
<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3> |
1341 | 6 |
|
6034 | 7 |
HOLCF is the definitional extension of Church's Higher-Order Logic with |
8 |
Scott's Logic for Computable Functions that has been implemented in the |
|
9 |
theorem prover Isabelle. This results in a flexible setup for reasoning |
|
10 |
about functional programs. HOLCF supports standard domain theory (in particular |
|
11 |
fixpoint reasoning and recursive domain equations) but also coinductive |
|
12 |
arguments about lazy datatypes. |
|
13 |
<P> |
|
14 |
The most recent description of HOLCF is found here: |
|
15 |
<UL> |
|
16 |
<li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A> |
|
17 |
</UL> |
|
1341 | 18 |
|
3279 | 19 |
A detailed description (in german) of the entire development can be found in: |
1341 | 20 |
|
21 |
<UL> |
|
15255 | 22 |
<li> <A HREF="http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf"> HOLCF: eine konservative Erweiterung von HOL um LCF</A>, <br> |
1410
324aa8134639
changed predicate flat to is_flat in theory Fix.thy
regensbu
parents:
1341
diff
changeset
|
23 |
<A HREF="http://www4.informatik.tu-muenchen.de/~regensbu/"> |
324aa8134639
changed predicate flat to is_flat in theory Fix.thy
regensbu
parents:
1341
diff
changeset
|
24 |
Franz Regenburger</A>. <br> |
324aa8134639
changed predicate flat to is_flat in theory Fix.thy
regensbu
parents:
1341
diff
changeset
|
25 |
Dissertation Technische Universität München. <BR> |
324aa8134639
changed predicate flat to is_flat in theory Fix.thy
regensbu
parents:
1341
diff
changeset
|
26 |
Year: 1994. |
324aa8134639
changed predicate flat to is_flat in theory Fix.thy
regensbu
parents:
1341
diff
changeset
|
27 |
</UL> |
324aa8134639
changed predicate flat to is_flat in theory Fix.thy
regensbu
parents:
1341
diff
changeset
|
28 |
|
3279 | 29 |
A short survey is available in: |
1410
324aa8134639
changed predicate flat to is_flat in theory Fix.thy
regensbu
parents:
1341
diff
changeset
|
30 |
<UL> |
15255 | 31 |
<li><A HREF="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</A> <br> |
1341 | 32 |
</UL> |
33 |
||
34 |
</BODY></HTML> |