|
| Titre : | Programming with higher-order logic [Texte imprimé] | | Type de document : | texte imprime | | Auteurs : | Dale Miller ; Gopalan Nadathur | | Editeur : | Cambridge : Cambridge University Press | | Année de publication : | 2012 | | Importance : | (XIII-306 p.) | | Format : | 24 cm | | ISBN/ISSN/EAN : | 978-0-521-87940-8 | | Note générale : | Bibliogr. p. 289-299. Index | | Langues : | Anglais | | Mots-clés : | Logic programming Prolog (Computer program language) Programmation logique Prolog (langage de programmation) | | Résumé : | Résumé(s) :
La 4e de couverture : "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"
Sommaire :
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, The Teyjus system | | Permalink : | ./index.php?lvl=notice_display&id=13873 |
Programming with higher-order logic [Texte imprimé] [texte imprime] / Dale Miller ; Gopalan Nadathur . - Cambridge : Cambridge University Press, 2012 . - (XIII-306 p.) ; 24 cm. ISBN : 978-0-521-87940-8 Bibliogr. p. 289-299. Index Langues : Anglais | Mots-clés : | Logic programming Prolog (Computer program language) Programmation logique Prolog (langage de programmation) | | Résumé : | Résumé(s) :
La 4e de couverture : "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"
Sommaire :
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, The Teyjus system | | Permalink : | ./index.php?lvl=notice_display&id=13873 |
| ![Programming with higher-order logic [Texte imprimé] vignette](./images/vide.png) |