The Resource Adapting Proofs-as-Programs : The Curry-Howard Protocol, by Iman Hafiz Poernomo, Martin Wirsing, John Newsome Crossley, (electronic resource)

Adapting Proofs-as-Programs : The Curry-Howard Protocol, by Iman Hafiz Poernomo, Martin Wirsing, John Newsome Crossley, (electronic resource)

Label
Adapting Proofs-as-Programs : The Curry-Howard Protocol
Title
Adapting Proofs-as-Programs
Title remainder
The Curry-Howard Protocol
Statement of responsibility
by Iman Hafiz Poernomo, Martin Wirsing, John Newsome Crossley
Creator
Contributor
Author
Author
Subject
Language
  • eng
  • eng
Summary
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 had the - tential for practical application to semi-automated software development. I- tial applications were mostly concerned with ?ne-grain, mathematical program synthesis. For various reasons, research interest in the area eventually tended toward more theoretic issues of constructive logic and type theory. However, in recent years, the situation has become more balanced, and 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. These applications constitute an exemplary justi?cation of the framework. Also, in and of themselves, these approaches to synthesis should be interesting for researchers working in the target problem domains
Member of
Is Subseries of
http://library.link/vocab/creatorName
Poernomo, Iman Hafiz
Dewey number
  • 511.3
  • 511.36
http://bibfra.me/vocab/relation/httpidlocgovvocabularyrelatorsaut
  • ZVsSSaAS8Tk
  • YKMhR2pPvj0
  • 9yr8fU1EyZs
Language note
English
LC call number
  • QA76.9.L63
  • QA76.5913
  • QA76.63
Literary form
non fiction
Nature of contents
dictionaries
http://library.link/vocab/relatedWorkOrContributorName
  • Wirsing, Martin.
  • Crossley, John Newsome.
Series statement
Monographs in Computer Science,
http://library.link/vocab/subjectName
  • Logic design
  • Logic, Symbolic and mathematical
  • Computer science
  • Software engineering
  • Logics and Meanings of Programs
  • Mathematical Logic and Foundations
  • Logic Design
  • Programming Techniques
  • Software Engineering/Programming and Operating Systems
  • Models and Principles
Label
Adapting Proofs-as-Programs : The Curry-Howard Protocol, by Iman Hafiz Poernomo, Martin Wirsing, John Newsome Crossley, (electronic resource)
Instantiates
Publication
Note
Description based upon print version of record
Bibliography note
Includes bibliographical references (p. [407]-416) and index
Carrier category
online resource
Carrier category code
  • cr
Content category
text
Content type code
  • txt
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
Dimensions
unknown
Extent
1 online resource (416 p.)
Form of item
online
Isbn
9786610851850
Media category
computer
Media type code
  • c
Other control number
10.1007/0-387-28183-5
Specific material designation
remote
System control number
  • (CKB)1000000000283668
  • (EBL)371311
  • (OCoLC)828801339
  • (SSID)ssj0000767764
  • (PQKBManifestationID)12370014
  • (PQKBTitleCode)TC0000767764
  • (PQKBWorkID)10758543
  • (PQKB)11116501
  • (SSID)ssj0000097116
  • (PQKBManifestationID)11111442
  • (PQKBTitleCode)TC0000097116
  • (PQKBWorkID)10114471
  • (PQKB)11721273
  • (DE-He213)978-0-387-28183-4
  • (MiAaPQ)EBC371311
  • (EXLCZ)991000000000283668
Label
Adapting Proofs-as-Programs : The Curry-Howard Protocol, by Iman Hafiz Poernomo, Martin Wirsing, John Newsome Crossley, (electronic resource)
Publication
Note
Description based upon print version of record
Bibliography note
Includes bibliographical references (p. [407]-416) and index
Carrier category
online resource
Carrier category code
  • cr
Content category
text
Content type code
  • txt
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
Dimensions
unknown
Extent
1 online resource (416 p.)
Form of item
online
Isbn
9786610851850
Media category
computer
Media type code
  • c
Other control number
10.1007/0-387-28183-5
Specific material designation
remote
System control number
  • (CKB)1000000000283668
  • (EBL)371311
  • (OCoLC)828801339
  • (SSID)ssj0000767764
  • (PQKBManifestationID)12370014
  • (PQKBTitleCode)TC0000767764
  • (PQKBWorkID)10758543
  • (PQKB)11116501
  • (SSID)ssj0000097116
  • (PQKBManifestationID)11111442
  • (PQKBTitleCode)TC0000097116
  • (PQKBWorkID)10114471
  • (PQKB)11721273
  • (DE-He213)978-0-387-28183-4
  • (MiAaPQ)EBC371311
  • (EXLCZ)991000000000283668

Library Locations

  • Architecture LibraryBorrow it
    Gould Hall 830 Van Vleet Oval Rm. 105, Norman, OK, 73019, US
    35.205706 -97.445050
  • Bizzell Memorial LibraryBorrow it
    401 W. Brooks St., Norman, OK, 73019, US
    35.207487 -97.447906
  • Boorstin CollectionBorrow it
    401 W. Brooks St., Norman, OK, 73019, US
    35.207487 -97.447906
  • Chinese Literature Translation ArchiveBorrow it
    401 W. Brooks St., RM 414, Norman, OK, 73019, US
    35.207487 -97.447906
  • Engineering LibraryBorrow it
    Felgar Hall 865 Asp Avenue, Rm. 222, Norman, OK, 73019, US
    35.205706 -97.445050
  • Fine Arts LibraryBorrow it
    Catlett Music Center 500 West Boyd Street, Rm. 20, Norman, OK, 73019, US
    35.210371 -97.448244
  • Harry W. Bass Business History CollectionBorrow it
    401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • History of Science CollectionsBorrow it
    401 W. Brooks St., Rm. 521NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • John and Mary Nichols Rare Books and Special CollectionsBorrow it
    401 W. Brooks St., Rm. 509NW, Norman, OK, 73019, US
    35.207487 -97.447906
  • Library Service CenterBorrow it
    2601 Technology Place, Norman, OK, 73019, US
    35.185561 -97.398361
  • Price College Digital LibraryBorrow it
    Adams Hall 102 307 West Brooks St., Norman, OK, 73019, US
    35.210371 -97.448244
  • Western History CollectionsBorrow it
    Monnet Hall 630 Parrington Oval, Rm. 300, Norman, OK, 73019, US
    35.209584 -97.445414
Processing Feedback ...