27 <dd>a new approach to verifying authentication protocols |
27 <dd>a new approach to verifying authentication protocols |
28 |
28 |
29 <dt>AxClasses |
29 <dt>AxClasses |
30 <dd>a few basic examples of using axiomatic type classes |
30 <dd>a few basic examples of using axiomatic type classes |
31 |
31 |
32 <dt>BCV |
32 <dt>Complex |
33 <dd>generic model of bytecode verification, i.e. data-flow analysis |
|
34 for assembly languages with subtypes |
|
35 |
|
36 <dt>HOL-Complex |
|
37 <dd>a development of the complex numbers, the reals, and the hyper-reals, |
33 <dd>a development of the complex numbers, the reals, and the hyper-reals, |
38 which are used in non-standard analysis (builds the image HOL-Complex) |
34 which are used in non-standard analysis (builds the image HOL-Complex) |
39 |
|
40 <dt>HOL-Complex-HahnBanach |
|
41 <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) |
|
42 |
|
43 <dt>HOL-Complex-ex |
|
44 <dd>miscellaneous real ans complex number examples |
|
45 |
35 |
46 <dt>Hoare |
36 <dt>Hoare |
47 <dd>verification of imperative programs (verification conditions are |
37 <dd>verification of imperative programs (verification conditions are |
48 generated automatically from pre/post conditions and loop invariants) |
38 generated automatically from pre/post conditions and loop invariants) |
|
39 |
|
40 <dt>HoareParallel |
|
41 <dd>verification of shared-variable imperative programs a la Owicki-Gries. |
|
42 (verification conditions are generated automatically) |
|
43 |
|
44 <dt>Hyperreal |
|
45 <dd>Nonstandard analysis. Builds on Real and is part of Complex. |
49 |
46 |
50 <dt>IMP |
47 <dt>IMP |
51 <dd>mechanization of a large part of a semantics text by Glynn Winskel |
48 <dd>mechanization of a large part of a semantics text by Glynn Winskel |
52 |
49 |
53 <dt>IMPP |
50 <dt>IMPP |
54 <dd>extension of IMP with local variables and mutually recursive |
51 <dd>extension of IMP with local variables and mutually recursive |
55 procedures |
52 procedures |
56 |
53 |
57 <dt>IOA |
54 <dt>Import |
58 <dd>a simple theory of Input/Output Automata |
55 <dd>theories imported from other (HOL) theorem provers. |
59 |
56 |
60 <dt>Induct |
57 <dt>Induct |
61 <dd>examples of (co)inductive definitions |
58 <dd>examples of (co)inductive definitions |
|
59 |
|
60 <dt>IOA |
|
61 <dd>a simple theory of Input/Output Automata |
62 |
62 |
63 <dt>Isar_examples |
63 <dt>Isar_examples |
64 <dd>several introductory examples using Isabelle/Isar |
64 <dd>several introductory examples using Isabelle/Isar |
65 |
65 |
66 <dt>Lambda |
66 <dt>Lambda |
67 <dd>fundamental properties of lambda-calculus (Church-Rosser and termination) |
67 <dd>fundamental properties of lambda-calculus (Church-Rosser and termination) |
68 |
68 |
69 <dt>Lattice |
69 <dt>Lattice |
70 <dd>lattices and order structures (in Isabelle/Isar) |
70 <dd>lattices and order structures (in Isabelle/Isar) |
71 |
71 |
|
72 <dt>Library |
|
73 <dd>A collection of generic theories |
|
74 |
|
75 <dt>Matrix |
|
76 <dd>two-dimensional matrices |
|
77 |
72 <dt>MicroJava |
78 <dt>MicroJava |
73 <dd>formalization of a fragment of Java, together with a corresponding |
79 <dd>formalization of a fragment of Java, together with a corresponding |
74 virtual machine and a specification of its bytecode verifier and a |
80 virtual machine and a specification of its bytecode verifier and a |
75 lightweight bytecode verifier, including proofs of type-safety. |
81 lightweight bytecode verifier, including proofs of type-safety |
76 |
82 |
77 <dt>Modelcheck |
83 <dt>Modelcheck |
78 <dd>basic setup for integration of some model checkers in Isabelle/HOL |
84 <dd>basic setup for integration of some model checkers in Isabelle/HOL |
79 |
85 |
|
86 <dt>NanoJava |
|
87 <dd>Haore Logic for a tiny fragment of Java |
|
88 |
80 <dt>NumberTheory |
89 <dt>NumberTheory |
81 <dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem, |
90 <dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem, |
82 Fermat/Euler Theorem, Wilson's Theorem |
91 Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity |
83 |
92 |
84 <dt>Prolog |
93 <dt>Prolog |
85 <dd>a (bare-bones) implementation of Lambda-Prolog |
94 <dd>a (bare-bones) implementation of Lambda-Prolog |
86 |
95 |
|
96 <dt>Real |
|
97 <dd>the real numbers, part of Complex |
|
98 |
|
99 <dt>Real/HahnBanach |
|
100 <dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) |
|
101 |
|
102 <dt>SET-Protocol |
|
103 <dd>verification of the SET Protocol |
|
104 |
87 <dt>Subst |
105 <dt>Subst |
88 <dd>defines a theory of substitution and unification. |
106 <dd>a theory of substitution and unification. |
89 |
107 |
90 <dt>TLA |
108 <dt>TLA |
91 <dd>Lamport's Temporal Logic of Actions (with separate example sessions) |
109 <dd>Lamport's Temporal Logic of Actions (with separate example sessions) |
92 |
110 |
93 <dt>UNITY |
111 <dt>UNITY |