{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T23:52:23Z","timestamp":1725580343023},"publisher-location":"Dordrecht","reference-count":17,"publisher":"Springer Netherlands","isbn-type":[{"type":"print","value":"9789400700796"},{"type":"electronic","value":"9789400700802"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-94-007-0080-2_6","type":"book-chapter","created":{"date-parts":[[2011,4,1]],"date-time":"2011-04-01T18:04:08Z","timestamp":1301681048000},"page":"81-97","source":"Crossref","is-referenced-by-count":0,"title":["What Is the Difference Between Proofs and Programs?"],"prefix":"10.1007","author":[{"given":"John N.","family":"Crossley","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,3,10]]},"reference":[{"key":"6_CR1","volume-title":"The Lambda Calculus, Its Syntax and Semantics","author":"P. H. Barendregt","year":"1995","unstructured":"Barendregt P. H. The Lambda Calculus, Its Syntax and Semantics. North Holland Publishing Company, Amsterdam, 1995."},{"key":"6_CR2","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"P. H. Barendregt","year":"1992","unstructured":"Barendregt P. H. Lambda calculi with types. In S. Abramsky and D. Gabbay and T. Maibaum, editors, Handbook of Logic in Computer Science, vol. 2, pages 117\u2013309 (Background: Computational Structures). Clarendon Press, Oxford, 1992."},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Berger U., and Schwichtenberg H. Program extraction from classical proofs. In D. Leivant, editor, Logic and Computational Complexity, International Workshop LCC \u201994, Indiapolis, IN, USA, October 1994, pages 77\u201397, 1995.","DOI":"10.1007\/3-540-60178-3_80"},{"key":"6_CR4","unstructured":"CoFI Language Design Task Group on Language Design. CASL, The Common Algebraic Specification Language, Summary, 25 March 2001, March 2001. Available at http:\/\/www.brics.dk\/Projects\/CoFI\/Documents\/CASL\/Summary\/ (accessed 3.i.05)"},{"key":"6_CR5","unstructured":"Crossley J. N. What is mathematical logic? A survey. Tutorial at the First International Conference on Logic and and its application to other disciplines, IIT Bombay, 2005, submitted for publication."},{"key":"6_CR6","unstructured":"Crossley J. N. Iman Poernomo, and Martin Wirsing. Extraction of structured programs from specification proofs. In D. Bert, C. Choppy, and P. Mosses, editors, Workshop on Algebraic Development Techniques, vol. 1827 of LNCS, pages 419\u2013437, 1999."},{"key":"6_CR7","doi-asserted-by":"publisher","first-page":"222","DOI":"10.1007\/978-1-4612-0325-4_8","volume-title":"Logical Methods: In honor of AnilNerode\u2019s Sixtieth Birthday","author":"J. N. Crossley","year":"1993","unstructured":"Crossley, J. N., and Shepherdson J. C. Extracting programs from proofs by an extension of the Curry-Howard process. In J. N. Crossley, J. B. Remmel, R. A. Shore, and M. E. Sweedler, editors, Logical Methods: In honor of AnilNerode\u2019s Sixtieth Birthday, pages 222\u2013288. Birkh\u00e4user, Boston, MA, 1993."},{"key":"6_CR8","volume-title":"Elements of Intuitionism","author":"M. Dummett","year":"1977","unstructured":"Dummett M. Elements of Intuitionism. Oxford University Press, Oxford, 1977."},{"key":"6_CR9","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538332.001.0001","volume-title":"Labelled Deductive Systems","author":"D. Gabbay","year":"1996","unstructured":"Gabbay D. Labelled Deductive Systems. Oxford University Press, Oxford, 1996."},{"key":"6_CR10","unstructured":"Girard J. Y. Interpr\u00e9tation functionelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tiqued\u2019ordre sup\u00e9rieure. PhD thesis, Universit\u00e9 Paris VII, Paris, 1972."},{"key":"6_CR11","volume-title":"Proofs and Types","author":"J. Y. Girard","year":"1989","unstructured":"Girard J. Y., Lafont Y., and Taylor P. Proofs and Types. Cambridge University Press, Cambridge, 1989."},{"issue":"10","key":"6_CR12","first-page":"576","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"Hoare C. A. R. An axiomatic basis for computer programming, Commun. Assoc Comput. Machinery, 1210: 576\u201380, 1969.","journal-title":"Commun. Assoc Comput. Machinery"},{"key":"6_CR13","first-page":"479","volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism","author":"W. Howard","year":"1969","unstructured":"Howard W. The formulae-as-types notion of construction. In J. R. Hindley and J. Seldin, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pages 479\u2013490. Academic Press, New York, NY, 1969."},{"key":"6_CR14","volume-title":"Introduction to Metamathematics","author":"S. C. Kleene","year":"1952","unstructured":"Kleene S. C. Introduction to Metamathematics. North-Holland, Amsterdam, 1952."},{"key":"6_CR15","unstructured":"Peterreins H. A natural-deduction-like calculus for structured specifications. PhD thesis, Ludwig-Maximilians-Universit\u00e4t, M\u00fcnchen, 1996."},{"key":"6_CR16","volume-title":"Adapting Proofs-Asprograms","author":"I. H. Poernomo","year":"2005","unstructured":"Poernomo I. H., Crossley J. N., and Wirsing M. Adapting Proofs-Asprograms. Springer, New York, NY, 2005."},{"key":"6_CR17","first-page":"269","volume-title":"Informatik und Mathematik, Festschrift f\u00fcr F. L. Bauer","author":"M. Wirsing","year":"1991","unstructured":"Wirsing M. Structured specifications: Syntax, semantics and proof calculus. In M. Broy, editor, Informatik und Mathematik, Festschrift f\u00fcr F. L. Bauer, pages 269\u2013283. Springer, Berlin, 1991."}],"container-title":["Proof, Computation and Agency"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-94-007-0080-2_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T17:15:56Z","timestamp":1712337356000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-94-007-0080-2_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9789400700796","9789400700802"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-94-007-0080-2_6","relation":{},"subject":[],"published":{"date-parts":[[2011]]}}}