HTML version of README
authorclasohm
Fri Nov 17 13:22:50 1995 +0100 (1995-11-17)
changeset 134169fec018854c
parent 1340 71b0a5d83347
child 1342 f6651b6b0482
HTML version of README
src/CTT/README.html
src/Cube/README.html
src/HOL/README.html
src/HOLCF/README.html
src/LCF/README.html
src/LK/README.html
src/Modal/README.html
src/ZF/README.html
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/CTT/README.html	Fri Nov 17 13:22:50 1995 +0100
     1.3 @@ -0,0 +1,32 @@
     1.4 +<HTML><HEAD><TITLE>CTT/ReadMe</TITLE></HEAD><BODY>
     1.5 +
     1.6 +<H2>CTT: Constructive Type Theory</H2>
     1.7 +
     1.8 +This directory contains the Standard ML sources of the Isabelle system for
     1.9 +Constructive Type Theory (extensional equality, no universes).  Important
    1.10 +files include
    1.11 +
    1.12 +<DL>
    1.13 +<DT>ROOT.ML
    1.14 +<DD>loads all source files.  Enter an ML image containing Pure
    1.15 +Isabelle and type: use "ROOT.ML";<P>
    1.16 +
    1.17 +<DT>Makefile
    1.18 +<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    1.19 +
    1.20 +<DT>ex
    1.21 +<DD>subdirectory containing examples.  To execute them, enter an ML image
    1.22 +containing CTT and type: use "ex/ROOT.ML";<P>
    1.23 +</DL>
    1.24 +
    1.25 +Useful references on Constructive Type Theory:
    1.26 +
    1.27 +<UL>
    1.28 +<LI>	B. Nordström, K. Petersson and J. M. Smith,<BR>
    1.29 +	Programming in Martin-Löf's Type Theory<BR>
    1.30 +	(Oxford University Press, 1990)
    1.31 +
    1.32 +<LI>	Simon Thompson,<BR>
    1.33 +	Type Theory and Functional Programming (Addison-Wesley, 1991)
    1.34 +</UL>
    1.35 +</BODY></HTML>
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Cube/README.html	Fri Nov 17 13:22:50 1995 +0100
     2.3 @@ -0,0 +1,31 @@
     2.4 +<HTML><HEAD><TITLE>Cube/ReadMe</TITLE></HEAD><BODY>
     2.5 +
     2.6 +<H2>Cube: Barendregt's Lambda-Cube</H2>
     2.7 +
     2.8 +This directory contains the Standard ML sources of the Isabelle system for
     2.9 +the Lambda-Cube.  Important files include
    2.10 +
    2.11 +<DL>
    2.12 +<DT>ROOT.ML
    2.13 +<DD>loads all source files.  Enter an ML image containing Pure
    2.14 +Isabelle and type: use "ROOT.ML";<P>
    2.15 +
    2.16 +<DT>Makefile
    2.17 +<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    2.18 +
    2.19 +<DT>ex
    2.20 +examples file. To execute them, enter an ML image
    2.21 +containing Cube and type: use "ex.ML";
    2.22 +</DL>
    2.23 +
    2.24 +NB: the formalization is not completely sound!  It does not enforce
    2.25 +distinctness of variable names in contexts!<P>
    2.26 +
    2.27 +For more information about the Lambda-Cube, see
    2.28 +
    2.29 +<UL>
    2.30 +<LI>H. Barendregt<BR>
    2.31 +    Introduction to Generalised Type Systems<BR>
    2.32 +    J. Functional Programming
    2.33 +</UL>
    2.34 +</BODY></HTML>
     3.1 --- a/src/HOL/README.html	Fri Nov 17 13:15:19 1995 +0100
     3.2 +++ b/src/HOL/README.html	Fri Nov 17 13:22:50 1995 +0100
     3.3 @@ -24,11 +24,12 @@
     3.4  Useful references on Higher-Order Logic:
     3.5  
     3.6  <UL>
     3.7 -<LI>P. B. Andrews, An Introduction to Mathematical Logic and Type Theory
     3.8 -(Academic Press, 1986).
     3.9 +<LI>P. B. Andrews,<BR>
    3.10 +    An Introduction to Mathematical Logic and Type Theory<BR>
    3.11 +    (Academic Press, 1986).
    3.12  
    3.13 -<LI>J. Lambek and P. J. Scott, Introduction to Higher Order
    3.14 -Categorical Logic (CUP, 1986)
    3.15 +<LI>J. Lambek and P. J. Scott,<BR>
    3.16 +    Introduction to Higher Order Categorical Logic (CUP, 1986)
    3.17  </UL>
    3.18  
    3.19  </BODY></HTML>
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOLCF/README.html	Fri Nov 17 13:22:50 1995 +0100
     4.3 @@ -0,0 +1,36 @@
     4.4 +<HTML><HEAD><TITLE>HOLCF/ReadMe</TITLE></HEAD><BODY>
     4.5 +
     4.6 +<H2>HOLCF: A higher order version of LCF based on Isabelle HOL</H2>
     4.7 +
     4.8 +Author:     Franz Regensburger<BR>
     4.9 +Copyright   1995 Technische Universität München<P>
    4.10 +
    4.11 +Version: 2.0<BR>
    4.12 +Date: 16.08.95<P>
    4.13 +
    4.14 +A detailed description of the entire development can be found in 
    4.15 +
    4.16 +<UL>
    4.17 +<LI>Franz Regensburger,<BR>
    4.18 +    HOLCF: Eine konservative Erweiterung von HOL um LCF,<BR>
    4.19 +    Dissertation, Technische Universität München, 1994
    4.20 +</UL>
    4.21 +
    4.22 +Changes:
    4.23 +
    4.24 +<DL>
    4.25 +<DT>14.10.94
    4.26 +<DD>New translation mechanism for continuous infixes
    4.27 +
    4.28 +<DT>18.05.95
    4.29 +<DD>Conversion to curried version of HOL.
    4.30 +
    4.31 +<DT>28.06.95
    4.32 +<DD>The old uncurried version of HOLCF is no longer supported
    4.33 +    in the distribution.
    4.34 +
    4.35 +<DT>18.08.95
    4.36 +<DD>added sections axioms, ops, domain, genertated
    4.37 +    and 8bit support
    4.38 +</DL>
    4.39 +</BODY></HTML>
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/LCF/README.html	Fri Nov 17 13:22:50 1995 +0100
     5.3 @@ -0,0 +1,27 @@
     5.4 +<HTML><HEAD><TITLE>LCF/ReadMe</TITLE></HEAD><BODY>
     5.5 +
     5.6 +<H2>LCF: Logic for Computable Functions</H2>
     5.7 +
     5.8 +This directory contains the Standard ML sources of the Isabelle system for
     5.9 +LCF.  It is loaded upon FOL, not Pure Isabelle.  Important files include
    5.10 +
    5.11 +<DL>
    5.12 +<DT>ROOT.ML
    5.13 +<DD>loads all source files.  Enter an ML image containing FOL
    5.14 +Isabelle and type: use "ROOT.ML";<P>
    5.15 +
    5.16 +<DT>Makefile
    5.17 +<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    5.18 +
    5.19 +<DT>ex.ML
    5.20 +<DD>file containing examples.  To execute it, enter an ML image
    5.21 +containing LCF and type:    use "ex.ML";
    5.22 +</DL>
    5.23 +
    5.24 +Useful references on First-Order Logic:
    5.25 +
    5.26 +<UL>
    5.27 +<LI>Lawrence C. Paulson,<BR>
    5.28 +    Logic and Computation: Interactive proof with Cambridge LCF (CUP, 1987)
    5.29 +</UL>
    5.30 +</BODY></HTML>
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/LK/README.html	Fri Nov 17 13:22:50 1995 +0100
     6.3 @@ -0,0 +1,30 @@
     6.4 +<HTML><HEAD><TITLE>LK/ReadMe</TITLE></HEAD><BODY>
     6.5 +
     6.6 +<H2>LK: Classical First-Order Sequent Calculus</H2>
     6.7 +
     6.8 +This directory contains the Standard ML sources of the Isabelle system for
     6.9 +First-Order Logic as a classical sequent calculus.  (For a Natural Deduction
    6.10 +version, see FOL.)  Important files include
    6.11 +
    6.12 +<DL>
    6.13 +<DT>ROOT.ML
    6.14 +<DD>loads all source files.  Enter an ML image containing Pure
    6.15 +Isabelle and type: use "ROOT.ML";<P>
    6.16 +
    6.17 +<DT>Makefile
    6.18 +<DD>compiles the files under Poly/ML or SML of New Jersey<P>
    6.19 +
    6.20 +<DT>ex
    6.21 +<DD>subdirectory containing examples.  To execute them, enter an ML image
    6.22 +containing LK and type: use "ex/ROOT.ML";<P>
    6.23 +</DL>
    6.24 +
    6.25 +Useful references on First-Order Logic:
    6.26 +
    6.27 +<UL>
    6.28 +<LI>Jean Gallier,<BR>
    6.29 +    Logic for Computer Science (Harper&Row, 1986)
    6.30 +<LI>G. Takeuti,<BR>
    6.31 +    Proof Theory (North Holland, 1987)
    6.32 +</UL>
    6.33 +</BODY></HTML>
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Modal/README.html	Fri Nov 17 13:22:50 1995 +0100
     7.3 @@ -0,0 +1,30 @@
     7.4 +<HTML><HEAD><TITLE>Modal/ReadMe</TITLE></HEAD><BODY>
     7.5 +
     7.6 +<H2>Modal: First-Order Modal Sequent Calculus</H2>
     7.7 +
     7.8 +This directory contains the Standard ML sources of the Isabelle system for
     7.9 +Modal Logic.  Important files include
    7.10 +
    7.11 +<DL>
    7.12 +<DT>ROOT.ML
    7.13 +<DD>loads all source files.  Enter an ML image containing LK
    7.14 +Isabelle and type: use "ROOT.ML";<P>
    7.15 +
    7.16 +<DT>ex
    7.17 +<DD>subdirectory containing examples.  Files Tthms.ML, S4thms.ML and
    7.18 +S43thms.ML contain the theorems of Modal Logics, so arranged since
    7.19 +T&lt;S4&lt;S43.  To execute them, enter an ML image containing Modal
    7.20 +and type: use "ex/ROOT.ML";
    7.21 +</DL>
    7.22 +
    7.23 +Thanks to Rajeev Gore' for supplying the inference system for S43.<P>
    7.24 +
    7.25 +Useful references on Modal Logics:
    7.26 +
    7.27 +<UL>
    7.28 +<LI>Melvin C Fitting,<BR>
    7.29 +    Proof Methods for Modal and Intuitionistic Logics (Reidel, 1983)
    7.30 +<LI>Lincoln A. Wallen,<BR>
    7.31 +    Automated Deduction in Nonclassical Logics (MIT Press, 1990)
    7.32 +</UL>
    7.33 +</BODY></HTML>
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/ZF/README.html	Fri Nov 17 13:22:50 1995 +0100
     8.3 @@ -0,0 +1,89 @@
     8.4 +<HTML><HEAD><TITLE>ZF/ReadMe</TITLE></HEAD><BODY>
     8.5 +
     8.6 +<H2>ZF: Zermelo-Fraenkel Set Theory</H2>
     8.7 +
     8.8 +This directory contains the Standard ML sources of the Isabelle system for
     8.9 +ZF Set Theory.  It is loaded upon FOL, not Pure Isabelle.  Important files
    8.10 +include
    8.11 +
    8.12 +<DL>
    8.13 +<DT>Makefile
    8.14 +<DD>compiles the files under Poly/ML or SML of New Jersey.  Can also
    8.15 +run all the tests described below.<P>
    8.16 +
    8.17 +<DT>ROOT.ML
    8.18 +<DD>loads all source files.  Enter an ML image containing FOL and
    8.19 +type: use "ROOT.ML";
    8.20 +</DL>
    8.21 +
    8.22 +There are also several subdirectories of examples.  To execute the examples on
    8.23 +some directory &lt;Dir&gt;, enter an ML image containing ZF and type
    8.24 +<TT>use "&lt;Dir&gt;/ROOT.ML";</TT>
    8.25 +
    8.26 +<DL>
    8.27 +<DT>AC
    8.28 +<DD>subdirectory containing proofs from the book "Equivalents of the Axiom
    8.29 +of Choice, II" by H. Rubin and J.E. Rubin, 1985.  Thanks to Krzysztof
    8.30 +Gr`abczewski.<P>
    8.31 +
    8.32 +<DT>Coind
    8.33 +<DD>subdirectory containing a large example of proof by co-induction.  It
    8.34 +is by Jacob Frost following a paper by Robin Milner and Mads Tofte.<P>
    8.35 +
    8.36 +<DT>IMP
    8.37 +<DD>subdirectory containing a semantics equivalence proof between
    8.38 +operational and denotational definitions of a simple programming language.
    8.39 +Thanks to Heiko Loetzbeyer & Robert Sandner.<P>
    8.40 +
    8.41 +<DT>Resid
    8.42 +<DD>subdirectory containing a proof of the Church-Rosser Theorem.  It is
    8.43 +by Ole Rasmussen, following the Coq proof by Gérard Huet.<P>
    8.44 +
    8.45 +<DT>ex
    8.46 +<DD>subdirectory containing various examples.
    8.47 +</DL>
    8.48 +
    8.49 +Isabelle/ZF formalizes the greater part of elementary set theory,
    8.50 +including relations, functions, injections, surjections, ordinals and
    8.51 +cardinals.  Results proved include Cantor's Theorem, the Recursion
    8.52 +Theorem, the Schroeder-Bernstein Theorem, and (assuming AC) the
    8.53 +Wellordering Theorem.<P>
    8.54 +
    8.55 +Isabelle/ZF also provides theories of lists, trees, etc., for
    8.56 +formalizing computational notions.  It supports inductive definitions
    8.57 +of infinite-branching trees for any cardinality of branching.<P>
    8.58 +
    8.59 +Useful references for Isabelle/ZF:
    8.60 +
    8.61 +<UL>
    8.62 +<LI>	Lawrence C. Paulson,<BR>
    8.63 +	Set theory for verification: I. From foundations to functions.<BR>
    8.64 +	J. Automated Reasoning 11 (1993), 353-389.
    8.65 +
    8.66 +<LI>	Lawrence C. Paulson,<BR>
    8.67 +	Set theory for verification: II. Induction and recursion.<BR>
    8.68 +	Report 312, Computer Lab (1993).<BR>
    8.69 +
    8.70 +<LI>	Lawrence C. Paulson,<BR>
    8.71 +	A fixedpoint approach to implementing (co)inductive definitions. <BR> 
    8.72 +	In: A. Bundy (editor),<BR>
    8.73 +	CADE-12: 12th International Conference on Automated Deduction,<BR>
    8.74 +	(Springer LNAI 814, 1994), 148-161.
    8.75 +</UL>
    8.76 +
    8.77 +Useful references on ZF set theory:
    8.78 +
    8.79 +<UL>
    8.80 +<LI>	Paul R. Halmos, Naive Set Theory (Van Nostrand, 1960)
    8.81 +
    8.82 +<LI>	Patrick Suppes, Axiomatic Set Theory (Dover, 1972)
    8.83 +
    8.84 +<LI>	Keith J. Devlin,<BR>
    8.85 +	Fundamentals of Contemporary Set Theory (Springer, 1979)
    8.86 +
    8.87 +<LI>	Kenneth Kunen<BR>
    8.88 +	Set Theory: An Introduction to Independence Proofs<BR>
    8.89 +	(North-Holland, 1980)
    8.90 +</UL>
    8.91 +
    8.92 +</BODY></HTML>