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

Avainsanat: COMPUTERS / Computer Science COM014000