src/HOLCF/README.html
author huffman
Wed, 02 Mar 2005 22:57:08 +0100
changeset 15563 9e125b675253
parent 15283 f21466450330
child 15582 7219facb3fd0
permissions -rw-r--r--
converted to new-style theory
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15283
f21466450330 DOCTYPE declaration added
webertj
parents: 15255
diff changeset
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
f21466450330 DOCTYPE declaration added
webertj
parents: 15255
diff changeset
     2
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2394
diff changeset
     3
<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     4
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2394
diff changeset
     5
<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
     6
6034
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
     7
HOLCF is the definitional extension of Church's Higher-Order Logic with
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
     8
Scott's Logic for Computable Functions that has been implemented in the
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
     9
theorem prover Isabelle.  This results in a flexible setup for reasoning
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    10
about functional programs. HOLCF supports standard domain theory (in particular
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    11
fixpoint reasoning and recursive domain equations) but also coinductive
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    12
arguments about lazy datatypes.
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    13
<P>
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    14
The most recent description of HOLCF is found here:
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    15
<UL>
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    16
<li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A>
96ac04a17c56 Link to HOLCF paper added.
nipkow
parents: 3279
diff changeset
    17
</UL>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    18
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2394
diff changeset
    19
A detailed description (in german) of the entire development can be found in:
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    20
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    21
<UL>
15255
1b860b5d23f8 fixed urls
nipkow
parents: 6034
diff changeset
    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>
1410
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    23
        <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
    24
        Franz Regenburger</A>. <br>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    25
        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
    26
        Year: 1994.
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    27
</UL>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    28
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 2394
diff changeset
    29
A short survey is available in:
1410
324aa8134639 changed predicate flat to is_flat in theory Fix.thy
regensbu
parents: 1341
diff changeset
    30
<UL>
15255
1b860b5d23f8 fixed urls
nipkow
parents: 6034
diff changeset
    31
<li><A HREF="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</A> <br>
1341
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    32
</UL>
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    33
69fec018854c HTML version of README
clasohm
parents:
diff changeset
    34
</BODY></HTML>