Research Catalog

Adapting proofs-as-programs : the Curry-Howard protocol

Title
Adapting proofs-as-programs : the Curry-Howard protocol / Iman Hafiz Poernomo, John Newsome Crossley, Martin Wirsing.
Author
Poernomo, Iman Hafiz, 1976-
Publication
New York : Springer Science+Business Media, [2005], ©2005.

Items in the Library & Off-site

Filter by

1 Item

StatusFormatAccessCall NumberItem Location
Request for On-site UseRequest Scan
How do I pick up this item and when will it be ready?
Book/TextRequest in advance QA9.54 .P64 2005Off-site

Holdings

Details

Additional Authors
  • Crossley, John N
  • Wirsing, M. (Martin)
Series Statement
Monographs in computer science
Uniform Title
Monographs in computer science.
Subject
  • Curry-Howard isomorphism
  • Proof theory
  • Logic, Symbolic and mathematical
  • Functional programming (Computer science)
  • Lambda calculus
  • Abstract data types (Computer science)
Bibliography (note)
  • Includes bibliographical references (p. [407]-416) and index.
Contents
1. Introduction -- 2. Functional program synthesis -- 3. The Curry-Howard protocol -- 4. Intuitionistic Hoare logic -- 5. Properties of intuitionistic Hoare logic -- 6. Proofs-as-imperative-programs -- 7. Reasoning about structured specifications -- 8. Proof-theoretic properties of SSL -- 9. Structured proofs-as-programs -- 10. Generic specifications -- 11. Structured program synthesis -- 12. Conclusions : toward constructive logic as a practical 4GL -- App. A. Constructive logic.
ISBN
0387237593 (hardback : acid-free paper)
LCCN
2005046411
OCLC
  • ocm58478542
  • SCSB-5205743
Owning Institutions
Columbia University Libraries