isabelle: src/HOL/HOLCF/README.html@0437dbc127b3 (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>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	26	<li><a href="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</a>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	27	</ul>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	28
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	29	A detailed description (in German) of the entire development can be found in:
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	30
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	31	<ul>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	32	<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	33	Franz Regensburger.<br>
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	34	Dissertation Technische Universität München.<br>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	35	Year: 1994.
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	36	</ul>
1410 324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	37
3279 815ef5848324 tuned all READMEs; wenzelm parents: 2394 diff changeset	38	A short survey is available in:
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	39	<ul>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	40	<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	41	</ul>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	42
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	43	</body>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	44
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	45	</html>

author	huffman
	Sat, 27 Nov 2010 16:08:10 -0800
changeset 40774	0437dbc127b3
parent 35174	src/HOLCF/README.html@e15040ae75d7
child 47839	3c54878ed67b
permissions	-rw-r--r--