# Item Details

- Item Actions

# Programming With Higher-Order Logic

Dale Miller, Gopalan Nadathur

- Format
- Book
- Published
- Cambridge ; New York : Cambridge University Press, 2012.
- Language
- English
- ISBN
- 9780521879408 (hbk.), 052187940X (hbk.)
- Related Resources
- Cover image

Contributor biographical information

Publisher description

Table of contents only - Summary
- "Formal systems that describe computations over syntactic structures occur frequently in computer science. Logic programming provides a natural framework for encoding and animating such systems. However, these systems often embody variable binding, a notion that must be treated carefully at a computational level. This book aims to show that a programming language based on a simply typed version of higher-order logic provides an elegant, declarative means for providing such a treatment. Three broad topics are covered in pursuit of this goal. First, a proof-theoretic framework that supports a general view of logic programming is identified. Second, an actual language called [Lambda]Prolog is developed by applying this view to higher-order logic. Finally, a methodology for programming with specifications is exposed by showing how several computations over formal objects such as logical formulas, functional programs, and [lambda]-terms and [pi]-calculus expressions can be encoded in [Lambda]Prolog"--Provided by publisher.
- Contents
- First-order terms and representations of data
- First-order horn clauses
- First-order hereditary Harrop formulas
- Typed [lambda] terms and formulas
- Using quantification at higher-order types
- Mechanisms for structuring large programs
- Computations over [lambda]-terms
- Unification of [lambda]-terms
- Implementing proof systems
- Computations over functional programs
- Encoding a process calculus language
- Appendix: The Teyjus system.

- Description
- xiii, 306 p. : ill. ; 24 cm.
- Notes
- Includes bibliographical references (p. 289-299) and index.
- Technical Details

## Availability

Library | Location | Map | Availability | Call Number |
---|---|---|---|---|

Brown Science and Engineering | Stacks | N/A | Available |
QA76.63 .M554 2012 |