src/HOL/HOLCF/README.html
changeset 40774 0437dbc127b3
parent 35174 e15040ae75d7
child 47839 3c54878ed67b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/README.html	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,45 @@
     1.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     1.5 +
     1.6 +<html>
     1.7 +
     1.8 +<head>
     1.9 +  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
    1.10 +  <title>HOLCF/README</title>
    1.11 +</head>
    1.12 +
    1.13 +<body>
    1.14 +
    1.15 +<h3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</h3>
    1.16 +
    1.17 +HOLCF is the definitional extension of Church's Higher-Order Logic with
    1.18 +Scott's Logic for Computable Functions that has been implemented in the
    1.19 +theorem prover Isabelle.  This results in a flexible setup for reasoning
    1.20 +about functional programs. HOLCF supports standard domain theory (in particular
    1.21 +fixpoint reasoning and recursive domain equations) but also coinductive
    1.22 +arguments about lazy datatypes.
    1.23 +
    1.24 +<p>
    1.25 +
    1.26 +The most recent description of HOLCF is found here:
    1.27 +
    1.28 +<ul>
    1.29 +  <li><a href="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</a>
    1.30 +</ul>
    1.31 +
    1.32 +A detailed description (in German) of the entire development can be found in:
    1.33 +
    1.34 +<ul>
    1.35 +  <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf">HOLCF: eine konservative Erweiterung von HOL um LCF</a>, <br>
    1.36 +      Franz Regensburger.<br>
    1.37 +      Dissertation Technische Universit&auml;t M&uuml;nchen.<br>
    1.38 +      Year: 1994.
    1.39 +</ul>
    1.40 +
    1.41 +A short survey is available in:
    1.42 +<ul>
    1.43 +  <li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</a><br>
    1.44 +</ul>
    1.45 +
    1.46 +</body>
    1.47 +
    1.48 +</html>