src/HOLCF/README.html
author nipkow
Fri Dec 18 19:43:10 1998 +0100 (1998-12-18)
changeset 6034 96ac04a17c56
parent 3279 815ef5848324
child 15255 1b860b5d23f8
permissions -rw-r--r--
Link to HOLCF paper added.
     1 <HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
     2 
     3 <H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
     4 
     5 HOLCF is the definitional extension of Church's Higher-Order Logic with
     6 Scott's Logic for Computable Functions that has been implemented in the
     7 theorem prover Isabelle.  This results in a flexible setup for reasoning
     8 about functional programs. HOLCF supports standard domain theory (in particular
     9 fixpoint reasoning and recursive domain equations) but also coinductive
    10 arguments about lazy datatypes.
    11 <P>
    12 The most recent description of HOLCF is found here:
    13 <UL>
    14 <li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A>
    15 </UL>
    16 
    17 A detailed description (in german) of the entire development can be found in:
    18 
    19 <UL>
    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>
    21         <A HREF="http://www4.informatik.tu-muenchen.de/~regensbu/">
    22         Franz Regenburger</A>. <br>
    23         Dissertation Technische Universit&auml;t M&uuml;nchen. <BR>
    24         Year: 1994.
    25 </UL>
    26 
    27 A short survey is available in:
    28 <UL>
    29 <li><A HREF="http://www4.informatik.tu-muenchen.de/papers/Regensburger_HOLT1995.ps.gz">HOLCF: Higher Order Logic of Computable Functions</A> <br>
    30 </UL>
    31 
    32 </BODY></HTML>