src/HOLCF/README.html
changeset 6034 96ac04a17c56
parent 3279 815ef5848324
child 15255 1b860b5d23f8
equal deleted inserted replaced
6033:c8c69a4a7762 6034:96ac04a17c56
     1 <HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
     1 <HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
     2 
     2 
     3 <H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
     3 <H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
     4 
     4 
     5 Author:     Franz Regensburger<BR>
     5 HOLCF is the definitional extension of Church's Higher-Order Logic with
     6 Copyright   1995 Technische Universität München<P>
     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>
     7 
    16 
     8 A detailed description (in german) of the entire development can be found in:
    17 A detailed description (in german) of the entire development can be found in:
     9 
    18 
    10 <UL>
    19 <UL>
    11   <li> <A HREF="http://www4.informatik.tu-muenchen.de/papers/Diss_Regensbu.ps.gz"> HOLCF: eine konservative Erweiterung von HOL um LCF</A>, <br>
    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>