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

• Κύριοι συγγραφείς: Poernomo, Iman Hafiz (Συγγραφέας), Wirsing, Martin (Συγγραφέας), Crossley, John Newsome (Συγγραφέας)
• Συγγραφή απο Οργανισμό/Αρχή: SpringerLink (Online service)
• Μορφή: Ηλεκτρονική πηγή Ηλ. βιβλίο
• Γλώσσα: English
• Έκδοση: New York, NY : Springer New York, 2005.
• Σειρά: Monographs in Computer Science,
• Θέματα: Computer science.; Logic design.; Software engineering.; Computer programming.; Computer logic.; Computers.; Mathematical logic.; Computer Science.; Logics and Meanings of Programs.; Mathematical Logic and Foundations.; Logic Design.; Programming Techniques.; Software Engineering/Programming and Operating Systems.; Models and Principles.

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

Πίνακας περιεχομένων:

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