Iman Hafiz Poernomo, John Newsome Crossley and Martin Wirsing Adapting Proofs-as-Programs—The Curry–Howard Protocol. Springer (2005). ISBN 0-387-23759-3. $79.95/£50.00/€64.95. 420 pp. Hardbound.
Pierre Castéran · The Computer Journal · 2005
The Curry–Howard isomorphism says that intuitionistic logic can be presented as a constructive type theory in which proofs correspond to terms, formulae to types, logical rules to type inference and proof normalization to term simplification. The proofs-as-programs paradigm consists in using the constructive information contained in the proofs to synthesize correct programs. In order to be useful, programs obtained by extraction must be optimized by erasing logical information which does not contribute to the wanted computations and must be written in ‘real’ programming languages. This book shows how to use proofs-as-programs with various programming paradigms. The book is divided in three main parts: Chapters 1–3 present an overview of the domain, and present the proof-as-programs paradigm in its best known configuration: pure SML functional programs are extracted from intuitionistic proofs. All the concepts that are used throughout the book are presented for the first time in Chapter 2: signatures, terms...