Detailansicht
Adapting Proofs-as-Programs
The Curry-Howard Protocol, Monographs in Computer Science
ISBN/EAN: 9780387237596
Umbreit-Nr.: 1906520
Sprache:
Englisch
Umfang: xii, 420 S., 54 s/w Illustr., 420 p. 54 illus.
Format in cm: 2.1 x 24 x 16
Einband:
gebundenes Buch
Erschienen am 21.06.2005
Auflage: 1/2005
- Zusatztext
- InhaltsangabePart 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.
- Kurztext
- Details several important advances in the direction of practical proofs-as-programs paradigm, which has applications in industrial-scale, complex software engineering problemsThe authors develop two novel applications in large-scale, coarse-grain software engineering problemsThe applications given in the book should be interesting for researchers working proofs-as-programs, logical frameworks, and computational logic