1  <ul>
2    <li>Higher-Order Logic</li>
3
4    <li style="list-style: none">
5      <ul>
6        <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
7        is a version of classical higher-order logic resembling
8        that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
9        </li>
10      </ul>
11    </li>
12  </ul>
13
14  <ul>
15    <li>First-Order Logic</li>
16
17    <li style="list-style: none">
18      <ul>
19        <li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
20        provides basic classical and intuitionistic first-order logic. It is
21        polymorphic.
22        </li>
23
24        <li><a href="ZF/index.html">ZF (Set Theory)</a>
25        offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
26        </li>
27
28        <li><a href="CCL/index.html">CCL (Classical Computational Logic)</a></li>
29
30        <li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a></li>
31
32        <li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a></li>
33      </ul>
34    </li>
35  </ul>
36
37  <ul>
38    <li>Miscellaneous</li>
39
40    <li style="list-style: none">
41      <ul>
42        <li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a></li>
43
44        <li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
45        is an extensional version of Martin-L&ouml;f's Type Theory.</li>
46
47        <li><a href="Cube/index.html">Cube (The Lambda Cube)</a></li>
48
49        <li><a href="Pure/Pure/index.html">The Pure logical framework</a></li>
50
51        <li><a href="Doc/index.html">Sources of Documentation</a></li>
52      </ul>
53    </li>
54  </ul>
55