Adapting Proofs-as-Programs

The Curry--Howard Protocol
 Previously published in hardcover
Besorgungstitel  |
 Lieferzeit: 3-5 Tage  
181,42 €

Alle Preise inkl. MwSt.
| zzgl. Versand
 
Part I. Prologue.- Introduction.- Part II. Generalizing Proofs-as-Programs.- Functional Program Synthesis.- The Curry--Howard protocol.- Part III. Imperative Proofs-as-Programs.- Intuitionistic Hoare Logic.- Properties of Intuitionistic Hoare Logic.- Proofs-as-Imperative-Programs.- Part IV. Structured Proofs-as-Programs.- Reasoning about Structured Specifications.- Proof-theoretic Properties of SSL.- Structured Proofs-as-Programs.- Generic Specifications.- Structured Program Synthesis.- Part V. Epilogue.- Conclusions: Toward Constructive Logic as a Practical 4GL.- Part VI. Appendix.- A: Constructive Logic.- References.- Index.
This monograph details several important advances in the direction of a practical proofs-as-programs paradigm, which constitutes a set of approaches to developing programs from proofs in constructive logic with applications to industrial-scale, complex software engineering problems. One of the books central themes is a general, abstract framework for developing new systems of programs synthesis by adapting proofs-as-programs to new contexts.
Autor: John N. Crossley, Iman Poernomo, Martin Wirsing
Prof. Dr. Martin Wirsing ist Leiter des Lehrstuhls für Programmierung und Software-Technik des Instituts für Informatik der LMU München und Vizepräsident der LMU für den Bereich Studium.

Zu diesem Artikel ist noch keine Rezension vorhanden.
Helfen sie anderen Besuchern und verfassen Sie selbst eine Rezension.

 

Rezensionen

Autor: John N. Crossley
ISBN-13 :: 9781441920140
ISBN: 1441920145
Erscheinungsjahr: 19.11.2010
Verlag: Springer New York
Gewicht: 649g
Seiten: 432
Sprache: Englisch
Auflage Softcover reprint of hardcover 1st ed. 2005.
Sonstiges: Taschenbuch, 235x155x23 mm
Google Plus
Powered by Inooga