Crossley, John Newsome
Adapting Proofs-as-Programs
Part I. Prologue
1. Introduction
Part II. Generalizing Proofs-as-Programs
2. Functional Program Synthesis
3. The Curry-Howard Protocol
Part III. Imperative Proofs-as-Programs
4. Intuitionistic Hoare Logic
5. Properties of Intuitionistic Hoare Logic
6. Proofs-as-Imperative-Programs
Part IV. Structured Proofs-as-Programs
7. Reasoning about Structured Specifications
8. Proof-theoretic Properties of SSL
9. Structured Proofs-as-Programs
10. Generic Specifications
11. Structured Program Synthesis
Part V. Epilogue
12. Conclusions: Toward Constructive Logic as a Practical 4GL
DRM-restrictions
Printing: not available
Clipboard copying: not available
Nyckelord: COMPUTERS / Computer Science COM014000
- Författare
- Crossley, John Newsome
- Poernomo, Iman Hafiz
- Wirsing, Martin
- Utgivare
- Springer
- Utgivningsår
- 2005
- Språk
- en
- Utgåva
- 1
- Kategori
- Datateknik, Datakommunikation
- Format
- E-bok
- eISBN (PDF)
- 9780387281834