{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:12:03Z","timestamp":1725664323604},"publisher-location":"Berlin, Heidelberg","reference-count":4,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540617808"},{"type":"electronic","value":"9783540707226"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_60","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:25:41Z","timestamp":1330295141000},"page":"36-46","source":"Crossref","is-referenced-by-count":6,"title":["The greatest common divisor: A case study for program extraction from classical proofs"],"prefix":"10.1007","author":[{"given":"U.","family":"Berger","sequence":"first","affiliation":[]},{"given":"H.","family":"Schwichtenberg","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"3_CR1","series-title":"volume 139 of Series F: Computer and Systems Sciences","first-page":"1","volume-title":"Proof and Computation","author":"U. Berger","year":"1995","unstructured":"Ulrich Berger and Helmut Schwichtenberg. Program development by proof transformation. In H. Schwichtenberg, editor, Proof and Computation, volume 139 of Series F: Computer and Systems Sciences, pages 1\u201345. NATO Advanced Study Institute, International Summer School held in Marktoberdorf, Germany, July 20\u2013August 1, 1993, Springer Verlag, Berlin, Heidelberg, New York, 1995."},{"key":"3_CR2","first-page":"77","volume-title":"volume 960 of Lecture Notes in Computer Science","author":"U. Berger","year":"1995","unstructured":"Ulrich Berger and Helmut Schwichtenberg. Program extraction from classical proofs. In D. Leivant, editor, Logic and Computational Complexity, International Workshop LCC '94, Indianapolis, IN, USA, October 1994, volume 960 of Lecture Notes in Computer Science, pages 77\u201397. Springer Verlag, Berlin, Heidelberg, New York, 1995."},{"key":"3_CR3","series-title":"volume 669 of Lecture Notes in Mathematics","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/BFb0103100","volume-title":"Higher Set Theory","author":"H. Friedman","year":"1978","unstructured":"Harvey Friedman. Classically and intuitionistically provably recursive functions. In D.S. Scott and G.H. M\u00fcller, editors, Higher Set Theory, volume 669 of Lecture Notes in Mathematics, pages 21\u201328. Springer Verlag, Berlin, Heidelberg, New York, 1978."},{"key":"3_CR4","first-page":"101","volume-title":"Constructivity in Mathematics","author":"G. Kreisel","year":"1959","unstructured":"Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pages 101\u2013128. North-Holland, Amsterdam, 1959."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61780-9_60.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:36:42Z","timestamp":1619573802000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":4,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}