src/HOLCF/README.html
author nipkow
Sun, 22 Dec 2002 10:43:43 +0100
changeset 13763 f94b569cd610
parent 6034 96ac04a17c56
child 15255 1b860b5d23f8
permissions -rw-r--r--
added print translations tha avoid eta contraction for important binders.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2394
diff changeset
     1
<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     2
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2394
diff changeset
     3
<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     4
6034
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
     5
HOLCF is the definitional extension of Church's Higher-Order Logic with
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
     6
Scott's Logic for Computable Functions that has been implemented in the
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
     7
theorem prover Isabelle.  This results in a flexible setup for reasoning
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
     8
about functional programs. HOLCF supports standard domain theory (in particular
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
     9
fixpoint reasoning and recursive domain equations) but also coinductive
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    10
arguments about lazy datatypes.
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    11
<P>
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    12
The most recent description of HOLCF is found here:
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    13
<UL>
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    14
<li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A>
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    15
</UL>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    16
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2394
diff changeset
    17
A detailed description (in german) of the entire development can be found in:
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    18
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    19
<UL>
1410
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    20
  <li> <A HREF="http://www4.informatik.tu-muenchen.de/papers/Diss_Regensbu.ps.gz"> HOLCF: eine konservative Erweiterung von HOL um LCF</A>, <br>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    21
        <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
    22
        Franz Regenburger</A>. <br>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    23
        Dissertation Technische Universit&auml;t M&uuml;nchen. <BR>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    24
        Year: 1994.
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    25
</UL>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    26
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2394
diff changeset
    27
A short survey is available in:
1410
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    28
<UL>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    29
<li><A HREF="http://www4.informatik.tu-muenchen.de/papers/Regensburger_HOLT1995.ps.gz">HOLCF: Higher Order Logic of Computable Functions</A> <br>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    30
</UL>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    31
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    32
</BODY></HTML>