isabelle: src/HOL/README.html@6ed42bcba707 (annotated)

2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	1	<!-- $Id$ -->
3279 815ef5848324 tuned all READMEs; wenzelm parents: 3125 diff changeset	2	<HTML><HEAD><TITLE>HOL/README</TITLE></HEAD><BODY>
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	3
3279 815ef5848324 tuned all READMEs; wenzelm parents: 3125 diff changeset	4	<H2>HOL: Higher-Order Logic</H2>
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	5
3279 815ef5848324 tuned all READMEs; wenzelm parents: 3125 diff changeset	6	This directory contains the ML sources of the Isabelle system for
815ef5848324 tuned all READMEs; wenzelm parents: 3125 diff changeset	7	Higher-Order Logic.<P>
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	8
3279 815ef5848324 tuned all READMEs; wenzelm parents: 3125 diff changeset	9	There are several subdirectories with examples:
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	10	<DL>
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	11	<DT>ex
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	12	<DD>general examples
12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	13
12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	14	<DT>Auth
12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	15	<DD>a new approach to verifying authentication protocols
12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	16
7303 96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	17	<DT>AxClasses
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	18	<DD>a few axiomatic type class examples:
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	19	<DL>
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	20
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	21	<DT> Tutorial <DD> Some simple axclass demos that go along with the
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	22	<em>axclass</em> Isabelle document (<tt>isatool doc axclass</tt>).
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	23
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	24	<DT> Group
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	25	<DD> Some bits of group theory.
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	26
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	27	<DT> Lattice
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	28	<DD> Basic theory of lattices and orders.
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	29
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	30	</DL>
96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	31
7691 b7e8277fa088 added BVC; wenzelm parents: 7662 diff changeset	32	<DT>BCV
b7e8277fa088 added BVC; wenzelm parents: 7662 diff changeset	33	<DD>generic model of bytecode verification, i.e. data-flow analysis
b7e8277fa088 added BVC; wenzelm parents: 7662 diff changeset	34	for assembly languages with subtypes.
b7e8277fa088 added BVC; wenzelm parents: 7662 diff changeset	35
7291 8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	36	<DT>Hoare
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	37	<DD>verification of imperative programs; verification conditions are
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	38	generated automatically from pre/post conditions and loop invariants.
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	39
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	40	<DT>IMP
12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	41	<DD>mechanization of a large part of a semantics text by Glynn Winskel
12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	42
3125 3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 2080 diff changeset	43	<DT>Induct
3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 2080 diff changeset	44	<DD>examples of (co)inductive definitions
3f0ab2c306f7 Moved induction examples to directory Induct paulson parents: 2080 diff changeset	45
7290 f1a37c379317 updated paulson parents: 4622 diff changeset	46	<DT>Integ
f1a37c379317 updated paulson parents: 4622 diff changeset	47	<DD>a development of the integers including efficient integer
f1a37c379317 updated paulson parents: 4622 diff changeset	48	calculations (part of the standard HOL environment)
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	49
12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	50	<DT>IOA
7291 8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	51	<DD>a simple theory of Input/Output Automata
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	52
7303 96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	53	<DT>Isar_examples
7983 d823fdcc0645 tuned; wenzelm parents: 7691 diff changeset	54	<DD>several introductory Isabelle/Isar examples
7303 96bc013c8987 AxClasses, Isar_examples; wenzelm parents: 7291 diff changeset	55
2080 12eed4cec935 Fuller description of examples paulson parents: 1341 diff changeset	56	<DT>Lambda
9811 39ffdb8cab03 HOL/Lambda: converted into new-style theory and document; wenzelm parents: 7983 diff changeset	57	<DD>fundamental properties of lambda-calculus (Church-Rosser and termination)
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	58
7291 8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	59	<DT>Lex
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	60	<DD>verification of a simple lexical analyzer generator
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	61
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	62	<DT>MiniML
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	63	<DD>formalization of type inference for the language Mini-ML
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	64
7290 f1a37c379317 updated paulson parents: 4622 diff changeset	65	<DT>Real
f1a37c379317 updated paulson parents: 4622 diff changeset	66	<DD>a development of the reals and hyper-reals, which are used in
f1a37c379317 updated paulson parents: 4622 diff changeset	67	non-standard analysis. Also includes the positive rationals. Used to build
f1a37c379317 updated paulson parents: 4622 diff changeset	68	the image HOL-Real.
f1a37c379317 updated paulson parents: 4622 diff changeset	69
7662 062a782d7402 Real/HahnBanach; wenzelm parents: 7303 diff changeset	70	<DT>Real/HahnBanach
062a782d7402 Real/HahnBanach; wenzelm parents: 7303 diff changeset	71	<DD>the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
062a782d7402 Real/HahnBanach; wenzelm parents: 7303 diff changeset	72
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	73	<DT>Subst
7290 f1a37c379317 updated paulson parents: 4622 diff changeset	74	<DD>defines a theory of substitution and unification.
f1a37c379317 updated paulson parents: 4622 diff changeset	75
7291 8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	76	<DT>TLA
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	77	<DD>Lamport's Temporal Logic of Actions
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	78
7290 f1a37c379317 updated paulson parents: 4622 diff changeset	79	<DT>Tools
f1a37c379317 updated paulson parents: 4622 diff changeset	80	<DD>holds code used to provide support for records, datatypes, induction, etc.
f1a37c379317 updated paulson parents: 4622 diff changeset	81
f1a37c379317 updated paulson parents: 4622 diff changeset	82	<DT>UNITY
f1a37c379317 updated paulson parents: 4622 diff changeset	83	<DD>Chandy and Misra's UNITY formalism.
7291 8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	84
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	85	<DT>W0
8aa66ddc0bea new entriues. nipkow parents: 7290 diff changeset	86	<DD>a precursor of MiniML, without let-expressions
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	87	</DL>
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	88
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	89	Useful references on Higher-Order Logic:
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	90
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	91	<UL>
4622 85aae356570c tuned; wenzelm parents: 3279 diff changeset	92
85aae356570c tuned; wenzelm parents: 3279 diff changeset	93	<LI> P. B. Andrews,<BR>
1341 69fec018854c HTML version of README clasohm parents: 1339 diff changeset	94	An Introduction to Mathematical Logic and Type Theory<BR>
69fec018854c HTML version of README clasohm parents: 1339 diff changeset	95	(Academic Press, 1986).
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	96
4622 85aae356570c tuned; wenzelm parents: 3279 diff changeset	97	<P>
85aae356570c tuned; wenzelm parents: 3279 diff changeset	98
85aae356570c tuned; wenzelm parents: 3279 diff changeset	99	<LI> A. Church,<BR>
85aae356570c tuned; wenzelm parents: 3279 diff changeset	100	A Formulation of the Simple Theory of Types<BR>
85aae356570c tuned; wenzelm parents: 3279 diff changeset	101	(Journal of Symbolic Logic, 1940).
85aae356570c tuned; wenzelm parents: 3279 diff changeset	102
85aae356570c tuned; wenzelm parents: 3279 diff changeset	103	<P>
85aae356570c tuned; wenzelm parents: 3279 diff changeset	104
85aae356570c tuned; wenzelm parents: 3279 diff changeset	105	<LI> M. J. C. Gordon and T. F. Melham (editors),<BR>
85aae356570c tuned; wenzelm parents: 3279 diff changeset	106	Introduction to HOL: A theorem proving environment for higher order logic<BR>
85aae356570c tuned; wenzelm parents: 3279 diff changeset	107	(Cambridge University Press, 1993).
85aae356570c tuned; wenzelm parents: 3279 diff changeset	108
85aae356570c tuned; wenzelm parents: 3279 diff changeset	109	<P>
85aae356570c tuned; wenzelm parents: 3279 diff changeset	110
85aae356570c tuned; wenzelm parents: 3279 diff changeset	111	<LI> J. Lambek and P. J. Scott,<BR>
85aae356570c tuned; wenzelm parents: 3279 diff changeset	112	Introduction to Higher Order Categorical Logic<BR>
85aae356570c tuned; wenzelm parents: 3279 diff changeset	113	(Cambridge University Press, 1986).
85aae356570c tuned; wenzelm parents: 3279 diff changeset	114
1339 f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	115	</UL>
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	116
f1a3a7b44ff1 converted README to HTLM; replaced "CHOL" by "HOL" clasohm parents: diff changeset	117	</BODY></HTML>

author	paulson
	Thu, 14 Sep 2000 11:34:13 +0200
changeset 9955	6ed42bcba707
parent 9811	39ffdb8cab03
child 10163	d1972b445ece
permissions	-rw-r--r--