Book contents
- Frontmatter
- Contents
- Preface
- Introduction
- 1 First-Order Terms and Representations of Data
- 2 First-Order Horn Clauses
- 3 First-Order Hereditary Harrop Formulas
- 4 Typed λ-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
- Bibliography
- Index
Bibliography
Published online by Cambridge University Press: 05 August 2012
- Frontmatter
- Contents
- Preface
- Introduction
- 1 First-Order Terms and Representations of Data
- 2 First-Order Horn Clauses
- 3 First-Order Hereditary Harrop Formulas
- 4 Typed λ-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
- Bibliography
- Index
Summary
- Type
- Chapter
- Information
- Programming with Higher-Order Logic , pp. 289 - 300Publisher: Cambridge University PressPrint publication year: 2012