| author | haftmann |
| Thu, 19 Jun 2025 17:15:40 +0200 | |
| changeset 82734 | 89347c0cc6a3 |
| parent 75916 | b6589c8ccadd |
| permissions | -rw-r--r-- |
|
75916
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
1 |
theory README imports Main |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
2 |
begin |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
3 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
4 |
section \<open>HOLCF: A higher-order version of LCF based on Isabelle/HOL\<close> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
5 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
6 |
text \<open> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
7 |
HOLCF is the definitional extension of Church's Higher-Order Logic with |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
8 |
Scott's Logic for Computable Functions that has been implemented in the |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
9 |
theorem prover Isabelle. This results in a flexible setup for reasoning |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
10 |
about functional programs. HOLCF supports standard domain theory (in |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
11 |
particular fixpoint reasoning and recursive domain equations) but also |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
12 |
coinductive arguments about lazy datatypes. |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
13 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
14 |
The most recent description of HOLCF is found here: |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
15 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
16 |
\<^item> \<^emph>\<open>HOLCF '11: A Definitional Domain Theory for Verifying Functional |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
17 |
Programs\<close> \<^url>\<open>http://web.cecs.pdx.edu/~brianh/phdthesis.html\<close>, Brian |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
18 |
Huffman. Ph.D. thesis, Portland State University. 2012. |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
19 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
20 |
Descriptions of earlier versions can also be found online: |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
21 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
22 |
\<^item> \<^emph>\<open>HOLCF = HOL+LCF\<close> \<^url>\<open>https://www21.in.tum.de/~nipkow/pubs/jfp99.html\<close> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
23 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
24 |
A detailed description (in German) of the entire development can be found |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
25 |
in: |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
26 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
27 |
\<^item> \<^emph>\<open>HOLCF: eine konservative Erweiterung von HOL um LCF\<close> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
28 |
\<^url>\<open>http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf\<close>, |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
29 |
Franz Regensburger. Dissertation Technische Universität München. 1994. |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
30 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
31 |
A short survey is available in: |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
32 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
33 |
\<^item> \<^emph>\<open>HOLCF: Higher Order Logic of Computable Functions\<close> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
34 |
\<^url>\<open>http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf\<close> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
35 |
\<close> |
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
36 |
|
|
b6589c8ccadd
discontinued special support for README.html (which was hardly ever used in the past 2 decades);
wenzelm
parents:
diff
changeset
|
37 |
end |