Programming with Higher-Order Logic

1. First-order terms and representations of data
2. First-order horn clauses
3. First-order hereditary Harrop formulas
4. Typed lambda terms and formulas
5. Using quantification at higher-order types
6. Mechanisms for structuring large programs
7. Computations over λ-terms
8. Unification of λ-terms
9. Implementing proof systems
10. Computations over functional programs
11. Encoding a process calculus language
Appendix: the Teyjus system.