Cover Image
Read Now

Adapting Proofs-as-Programs The Curry--Howard Protocol

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 ha...

Full description

Bibliographic Details
Main Authors: Poernomo, Iman, Crossley, John N. (Author), Wirsing, Martin (Author)
Format: eBook
Language:English
Published: New York, NY Springer New York 2005, 2005
Edition:1st ed. 2005
Series:Monographs in Computer Science
Subjects:
Computer Science Logic And Foundations Of Programming
Models Of Computation
Software Engineering
Programming Techniques
Computer Science
Computer Programming
Mathematical Logic
Logic Design
Mathematical Logic And Foundations
Online Access:
Collection: Springer eBooks 2005- - Collection details see MPG.ReNa
Table of Contents:
  • Prologue
  • Generalizing Proofs-as-Programs
  • Functional Program Synthesis
  • The Curry-Howard Protocol
  • Imperative Proofs-as-Programs
  • Intuitionistic Hoare Logic
  • Properties of Intuitionistic Hoare Logic
  • Proofs-as-Imperative-Programs
  • Structured Proofs-as-Programs
  • Reasoning about Structured Specifications
  • Proof-theoretic Properties of SSL
  • Structured Proofs-as-Programs
  • Generic Specifications
  • Structured Program Synthesis
  • Epilogue
  • Conclusions: Toward Constructive Logic as a Practical 4GL.

Similar Items