Table of contents

The full table of contents is available as a pdf. The main chapter titles are listed below.

Preface

Introduction

Chapter 1 First-Order Terms and Representations of Data

Chapter 2 First-Order Horn Clauses

Chapter 3 First-Order Hereditary Harrop Formulas

Chapter 4 Typed λ-Terms and Formulas

Chapter 5 Using Quantification at Higher-Order Types

Chapter 6 Mechanisms for Structuring Large Programs

Chapter 7 Computations over λ-Terms

Chapter 8 Unification of λ-Terms

Chapter 9 Implementing Proof Systems

Chapter 10 Computations over Functional Programs

Chapter 11 Encoding a Process Calculus Language

Appendix A The Teyjus System