Skip to main content
SpringerLink
Log in
Book cover

Adapting Proofs-as-Programs

The Curry--Howard Protocol

  • Book
  • © 2005

Overview

Authors:
  1. Iman Hafiz Poernomo

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

    View author publications

    You can also search for this author in PubMed   Google Scholar

  2. Martin Wirsing

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

    View author publications

    You can also search for this author in PubMed   Google Scholar

  3. John Newsome Crossley

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

    View author publications

    You can also search for this author in PubMed   Google Scholar

  • Details several important advances in the direction of practical proofs-as-programs paradigm, which has applications in industrial-scale, complex software engineering problems
  • The authors develop two novel applications in large-scale, coarse-grain software engineering problems
  • The applications given in the book should be interesting for researchers working proofs-as-programs, logical frameworks, and computational logic

Part of the book series: Monographs in Computer Science (MCS)

This is a preview of subscription content, log in via an institution to check access.

Access this book

Log in via an institution
eBook USD 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (12 chapters)

  1. Front Matter

    Pages i-xi
    Download chapter PDF

  2. Prologue

    1. Front Matter

      Pages 1-1
      Download chapter PDF

    2. Introduction

      Pages 3-21

  3. Generalizing Proofs-as-Programs

    1. Front Matter

      Pages 23-23
      Download chapter 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
      Download chapter 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
      Download chapter 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
      Download chapter PDF

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

      Pages 393-396

  7. Back Matter

    Pages 397-420
    Download chapter PDF
Back to top

Keywords

About this book

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.

Reviews

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)

Authors and Affiliations

  • 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

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation