isabelle: src/HOL/HOLCF/README.html@03aa1b63af10 (annotated)

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
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	3	<html>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	4
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	5	<head>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	6	<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	7	<title>HOLCF/README</title>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	8	</head>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	9
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	10	<body>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	11
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	12	<h3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</h3>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	13
6034 96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	14	HOLCF is the definitional extension of Church's Higher-Order Logic with
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	15	Scott's Logic for Computable Functions that has been implemented in the
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	16	theorem prover Isabelle. This results in a flexible setup for reasoning
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	17	about functional programs. HOLCF supports standard domain theory (in particular
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	18	fixpoint reasoning and recursive domain equations) but also coinductive
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	19	arguments about lazy datatypes.
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	20
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	21	<p>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	22
6034 96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	23	The most recent description of HOLCF is found here:
1341 69fec018854c HTML version of README clasohm parents: diff changeset	24
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	25	<ul>
47839 3c54878ed67b update references in HOLCF README huffman parents: 40774 diff changeset	26	<li><a href="http://web.cecs.pdx.edu/~brianh/phdthesis.html">HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs</a>, <br>
3c54878ed67b update references in HOLCF README huffman parents: 40774 diff changeset	27	Brian Huffman.<br>
3c54878ed67b update references in HOLCF README huffman parents: 40774 diff changeset	28	Ph.D. thesis, Portland State University.<br>
3c54878ed67b update references in HOLCF README huffman parents: 40774 diff changeset	29	Year: 2012.
3c54878ed67b update references in HOLCF README huffman parents: 40774 diff changeset	30	</ul>
3c54878ed67b update references in HOLCF README huffman parents: 40774 diff changeset	31
3c54878ed67b update references in HOLCF README huffman parents: 40774 diff changeset	32	Descriptions of earlier versions can also be found online:
3c54878ed67b update references in HOLCF README huffman parents: 40774 diff changeset	33
3c54878ed67b update references in HOLCF README huffman parents: 40774 diff changeset	34	<ul>
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	35	<li><a href="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</a>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	36	</ul>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	37
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	38	A detailed description (in German) of the entire development can be found in:
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	39
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	40	<ul>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	41	<li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Diss_Regensbu.pdf">HOLCF: eine konservative Erweiterung von HOL um LCF</a>, <br>
24567 4970fb01aa01 typo fixed, dead link removed webertj parents: 15582 diff changeset	42	Franz Regensburger.<br>
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	43	Dissertation Technische Universität München.<br>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	44	Year: 1994.
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	45	</ul>
1410 324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	46
3279 815ef5848324 tuned all READMEs; wenzelm parents: 2394 diff changeset	47	A short survey is available in:
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	48	<ul>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	49	<li><a href="http://www4.informatik.tu-muenchen.de/publ/papers/Regensburger_HOLT1995.pdf">HOLCF: Higher Order Logic of Computable Functions</a><br>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	50	</ul>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	51
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	52	</body>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	53
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	54	</html>

author	wenzelm
	Sat, 14 Mar 2015 16:56:11 +0100
changeset 59692	03aa1b63af10
parent 47839	3c54878ed67b
permissions	-rw-r--r--