Item Details
Programming With HigherOrder 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 higherorder logic provides an elegant, declarative means for providing such a treatment. Three broad topics are covered in pursuit of this goal. First, a prooftheoretic 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 higherorder 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
 Firstorder terms and representations of data
 Firstorder horn clauses
 Firstorder hereditary Harrop formulas
 Typed [lambda] terms and formulas
 Using quantification at higherorder 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. 289299) and index.
 Technical Details

 Access in Virgo Classic
 Staff View
LEADER 03102cam a2200433 a 4500001 u5814440003 SIRSI005 20120926133130.0008 120427s2012 enka b 001 0 enga 2012016719a 9780521879408 (hbk.)a 052187940X (hbk.)a (OCoLC)774491609a DLC b eng c DLC d YDX d BTCTA d OCLCO d UKMGB d CDX d YDXCP d BWX d IUL d PUL d CDXa pcca QA76.63 b .M554 2012a 005.1/15 2 23a Miller, Dale q (Dale A.)a Programming with higherorder logic / c Dale Miller, Gopalan Nadathur.a Cambridge ; a New York : b Cambridge University Press, c 2012.a xiii, 306 p. : b ill. ; c 24 cm.a Includes bibliographical references (p. 289299) and index.a Firstorder terms and representations of data  Firstorder horn clauses  Firstorder hereditary Harrop formulas  Typed [lambda] terms and formulas  Using quantification at higherorder 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.a "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 higherorder logic provides an elegant, declarative means for providing such a treatment. Three broad topics are covered in pursuit of this goal. First, a prooftheoretic 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 higherorder 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.a Logic programming.a Prolog (Computer program language)a Nadathur, Gopalan.3 Cover image u http://proxy01.its.virginia.edu/login?url=http://assets.cambridge.org/97805218/79408/cover/9780521879408.jpg3 Contributor biographical information u http://catdir.loc.gov/catdir/enhancements/fy1210/2012016719b.html3 Publisher description u http://catdir.loc.gov/catdir/enhancements/fy1210/2012016719d.html3 Table of contents only u http://catdir.loc.gov/catdir/enhancements/fy1210/2012016719t.htmla 5a QA76.63 .M554 2012 w LC i X030844117 l STACKS m SCIENG t BOOK
Availability
Library  Location  Map  Availability  Call Number 

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