src/HOLCF/README.html
author webertj
Sun Nov 14 01:40:27 2004 +0100 (2004-11-14)
changeset 15283 f21466450330
parent 15255 1b860b5d23f8
child 15582 7219facb3fd0
permissions -rw-r--r--
DOCTYPE declaration added
webertj@15283
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
webertj@15283
     2
wenzelm@3279
     3
<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
clasohm@1341
     4
wenzelm@3279
     5
<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
clasohm@1341
     6
nipkow@6034
     7
HOLCF is the definitional extension of Church's Higher-Order Logic with
nipkow@6034
     8
Scott's Logic for Computable Functions that has been implemented in the
nipkow@6034
     9
theorem prover Isabelle.  This results in a flexible setup for reasoning
nipkow@6034
    10
about functional programs. HOLCF supports standard domain theory (in particular
nipkow@6034
    11
fixpoint reasoning and recursive domain equations) but also coinductive
nipkow@6034
    12
arguments about lazy datatypes.
nipkow@6034
    13
<P>
nipkow@6034
    14
The most recent description of HOLCF is found here:
nipkow@6034
    15
<UL>
nipkow@6034
    16
<li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A>
nipkow@6034
    17
</UL>
clasohm@1341
    18
wenzelm@3279
    19
A detailed description (in german) of the entire development can be found in:
clasohm@1341
    20
clasohm@1341
    21
<UL>
nipkow@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>
regensbu@1410
    23
        <A HREF="http://www4.informatik.tu-muenchen.de/~regensbu/">
regensbu@1410
    24
        Franz Regenburger</A>. <br>
regensbu@1410
    25
        Dissertation Technische Universit&auml;t M&uuml;nchen. <BR>
regensbu@1410
    26
        Year: 1994.
regensbu@1410
    27
</UL>
regensbu@1410
    28
wenzelm@3279
    29
A short survey is available in:
regensbu@1410
    30
<UL>
nipkow@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>
clasohm@1341
    32
</UL>
clasohm@1341
    33
clasohm@1341
    34
</BODY></HTML>