Research Catalog

Programming with higher-order logic

Title
Programming with higher-order logic / Dale Miller, INRIA-Saclay, Île de France & LIX, École Polytechnique, Gopalan Nadathur, University of Minnesota.
Author
Miller, Dale (Dale A.)
Publication
New York, NY : Cambridge University Press, 2012.

Items in the Library & Off-site

Filter by

1 Item

StatusFormatAccessCall NumberItem Location
Request for On-site UseRequest Scan
How do I pick up this item and when will it be ready?
TextUse in library QA76.63 .M554 2012Off-site

Details

Additional Authors
Nadathur, Gopalan.
Description
xiii, 306 pages; 24 cm
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.
Subject
  • Logic programming
  • Prolog (Computer program language)
  • COMPUTERS > Programming Languages > General
  • PROLOG Programmiersprache
  • Logische Programmierung
Bibliography (note)
  • Includes bibliographical references and index.
Contents
Machine generated contents note: 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 [lambda]-terms; 8. Unification of [lambda]-terms; 9. Implementing proof systems; 10. Computations over functional programs; 11. Encoding a process calculus language; Appendix A. The Teyjus system.
ISBN
  • 9780521879408
  • 052187940X
LCCN
2012016719
OCLC
  • ocn774491609
  • 774491609
  • SCSB-9171741
Owning Institutions
Princeton University Library