Adapting Proofs-as-Programs : The Curry--Howard Protocol
- Author
- Iman Hafiz Poernomo, Martin Wirsing, John Newsome Crossley
- Publication Year
- 2005
- Publisher
- Springer
- Language
- English
- Document Type
- Book
- Faculty / Subject Heading
- Computer Science
- Download Book Read book
This book nuds 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. 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.
Keywords: Computer science / Computer / Computer science / Formal method / Formal methods / Logic / Program synthesis / Proof / Software / Software engineering / Type theory
