Adapting Proofs-as-Programs

1. Front Matter

   Pages i-xi

   PDF

2. Prologue

   1. Front Matter

      Pages 1-1

      PDF

   2. Introduction

      Pages 3-21

3. Generalizing Proofs-as-Programs

   1. Front Matter

      Pages 23-23

      PDF

   2. Functional Program Synthesis

      Pages 25-75

   3. The Curry-Howard Protocol

      Pages 77-89

4. Imperative Proofs-as-Programs

   1. Front Matter

      Pages 91-94

      PDF

   2. Intuitionistic Hoare Logic

      Pages 95-134

   3. Properties of Intuitionistic Hoare Logic

      Pages 135-164

   4. Proofs-as-Imperative-Programs

      Pages 165-213

5. Structured Proofs-as-Programs

   1. Front Matter

      Pages 215-215

      PDF

   2. Reasoning about Structured Specifications

      Pages 217-252

   3. Proof-theoretic Properties of SSL

      Pages 253-295

   4. Structured Proofs-as-Programs

      Pages 297-339

   5. Generic Specifications

      Pages 341-365

   6. Structured Program Synthesis

      Pages 367-389

6. Epilogue

   1. Front Matter

      Pages 391-391

      PDF

   2. Conclusions: Toward Constructive Logic as a Practical 4GL

      Pages 393-396

7. Back Matter

   Pages 397-420

   PDF

This book ?nds new things to do with an old idea. The proofs-as-programs paradigm constitutes a set of approaches to developing programs from proofs in constructive logic. It has been over thirty years since the paradigm was ?rst conceived. At that time, there was a belief that proofs-as-programs had the - tential for practical application to semi-automated software development. I- tial applications were mostly concerned with ?ne-grain, mathematical program synthesis. For various reasons, research interest in the area eventually tended toward more theoretic issues of constructive logic and type theory. However, in recent years, the situation has become more balanced, and there is increasingly active research in applying constructive techniques to industrial-scale, complex software engineering problems. Thismonographdetailsseveralimportantadvancesinthisdirectionofpr- tical proofs-as-programs. One of the central themes of the book is a general, abstract framework for developing new systems of program synthesis by adapting proofs-as-programs to new contexts. Framework-oriented approaches that facilitate analogous - proaches to building systems for solving particular problems have been popular and successful. Thesemethodsarehelpful asthey providea formal toolbox that enablesa“roll-your-own”approachtodevelopingsolutions.Itishopedthatour framework will have a similar impact. The framework is demonstrated by example. We will give two novel - plications of proofs-as-programs to large-scale, coarse-grain software engine- ing problems: contractual imperative program synthesis and structured p- gram synthesis. These applications constitute an exemplary justi?cation of the framework. Also, in and of themselves, these approaches to synthesis should be interesting forresearchers working in the target problem domains.

• computer
• computer science
• formal method
• formal methods
• logic
• program synthesis
• proof
• software
• software engineering
• type theory

From the reviews:

"This monograph serves the dual purpose of providing a state-of-the-art overview of the field and detailing tools and techniques to stimulate further research. It can serve as material for graduate students in computer science or mathematics, the proofs-as-programs research community and the computational logic, formal methods and software engineering communities." (Doina Tatar, Zentralblatt MATH, Vol. 1095 (21), 2006)

• Department of Computer Science, King’s College London Strand, London, UK

  Iman Hafiz Poernomo

• Institut für Informatik, Ludwig-Maximilians Universitat München, München, Germany

  Martin Wirsing

• School of Computer Science and Software Engineering, Monash University, Victoria, Australia

  John Newsome Crossley

Policies and ethics