isabelle: src/HOLCF/README.html@033831fd9ef3 (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	<!-- $Id$ -->
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	4
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	5	<html>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	6
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	7	<head>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	8	<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	9	<title>HOLCF/README</title>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	10	</head>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	11
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	12	<body>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	13
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	14	<h3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</h3>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	15
6034 96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	16	HOLCF is the definitional extension of Church's Higher-Order Logic with
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	17	Scott's Logic for Computable Functions that has been implemented in the
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	18	theorem prover Isabelle. This results in a flexible setup for reasoning
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	19	about functional programs. HOLCF supports standard domain theory (in particular
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	20	fixpoint reasoning and recursive domain equations) but also coinductive
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	21	arguments about lazy datatypes.
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	22
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	23	<p>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	24
6034 96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	25	The most recent description of HOLCF is found here:
1341 69fec018854c HTML version of README clasohm parents: diff changeset	26
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	27	<ul>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	28	<li><a href="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</a>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	29	</ul>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	30
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	31	A detailed description (in German) of the entire development can be found in:
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	32
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	33	<ul>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	34	<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	35	Franz Regensburger.<br>
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	36	Dissertation Technische Universität München.<br>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	37	Year: 1994.
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	38	</ul>
1410 324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	39
3279 815ef5848324 tuned all READMEs; wenzelm parents: 2394 diff changeset	40	A short survey is available in:
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	41	<ul>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	42	<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	43	</ul>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	44
15582 7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	45	</body>
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	46
7219facb3fd0 HTML 4.01 Transitional conformity webertj parents: 15283 diff changeset	47	</html>

author	huffman
	Thu, 19 Nov 2009 22:25:11 -0800
changeset 33809	033831fd9ef3
parent 24567	4970fb01aa01
child 35174	e15040ae75d7
permissions	-rw-r--r--