isabelle: src/HOLCF/README.html@2c64c7991f7c (annotated)

3279 815ef5848324 tuned all READMEs; wenzelm parents: 2394 diff changeset	1	<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	2
3279 815ef5848324 tuned all READMEs; wenzelm parents: 2394 diff changeset	3	<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	4
6034 96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	5	HOLCF is the definitional extension of Church's Higher-Order Logic with
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	6	Scott's Logic for Computable Functions that has been implemented in the
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	7	theorem prover Isabelle. This results in a flexible setup for reasoning
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	8	about functional programs. HOLCF supports standard domain theory (in particular
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	9	fixpoint reasoning and recursive domain equations) but also coinductive
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	10	arguments about lazy datatypes.
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	11	<P>
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	12	The most recent description of HOLCF is found here:
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	13	<UL>
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	14	<li> <A HREF="/~nipkow/pubs/jfp99.html">HOLCF = HOL+LCF</A>
96ac04a17c56 Link to HOLCF paper added. nipkow parents: 3279 diff changeset	15	</UL>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	16
3279 815ef5848324 tuned all READMEs; wenzelm parents: 2394 diff changeset	17	A detailed description (in german) of the entire development can be found in:
1341 69fec018854c HTML version of README clasohm parents: diff changeset	18
69fec018854c HTML version of README clasohm parents: diff changeset	19	<UL>
1410 324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	20	<li> <A HREF="http://www4.informatik.tu-muenchen.de/papers/Diss_Regensbu.ps.gz"> HOLCF: eine konservative Erweiterung von HOL um LCF</A>, <br>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	21	<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	22	Franz Regenburger</A>. <br>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	23	Dissertation Technische Universität München. <BR>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	24	Year: 1994.
324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	25	</UL>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	26
3279 815ef5848324 tuned all READMEs; wenzelm parents: 2394 diff changeset	27	A short survey is available in:
1410 324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	28	<UL>
324aa8134639 changed predicate flat to is_flat in theory Fix.thy regensbu parents: 1341 diff changeset	29	<li><A HREF="http://www4.informatik.tu-muenchen.de/papers/Regensburger_HOLT1995.ps.gz">HOLCF: Higher Order Logic of Computable Functions</A> <br>
1341 69fec018854c HTML version of README clasohm parents: diff changeset	30	</UL>
69fec018854c HTML version of README clasohm parents: diff changeset	31
69fec018854c HTML version of README clasohm parents: diff changeset	32	</BODY></HTML>

author	paulson
	Wed, 10 Jan 2001 12:43:40 +0100
changeset 10853	2c64c7991f7c
parent 6034	96ac04a17c56
child 15255	1b860b5d23f8
permissions	-rw-r--r--