{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T11:03:38Z","timestamp":1743073418152,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678984"},{"type":"electronic","value":"9783540446163"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/978-3-540-44616-3_24","type":"book-chapter","created":{"date-parts":[[2010,10,14]],"date-time":"2010-10-14T14:09:44Z","timestamp":1287065384000},"page":"419-437","source":"Crossref","is-referenced-by-count":3,"title":["Extraction of Structured Programs from Specification Proofs"],"prefix":"10.1007","author":[{"given":"John N.","family":"Crossley","sequence":"first","affiliation":[]},{"given":"Iman","family":"Poernomo","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Wirsing","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Albrecht, D.W., Crossley, J.N.: Program extraction, simplified proof-terms and realizability, Technical Report 271, Dept of Computer Science, Monash University, Australia (1997)"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1007\/3-540-58156-1_42","volume-title":"Automated Deduction - CADE-12","author":"P. Anderson","year":"1994","unstructured":"Anderson, P.: Representing proof transformations for program optimization. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 575\u2013590. Springer, Heidelberg (1994)"},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1006\/inco.1996.0025","volume":"125","author":"F. Barbanera","year":"1996","unstructured":"Barbanera, F., Berardi, S.: A Symmetric Lambda-Calculus for \u201cClassical\u201d Program Extraction\u201d. Information and Computation\u00a0125, 103\u2013117 (1996)","journal-title":"Information and Computation"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Berger, U., Schwichtenberg, H.: Program development by Proof Transformation. In: Proceedings of the NATO Advanced Study Institute on Proof and Computation, Marktoberdorf, Germany (1993); published in cooperation with the NATO Scientific Affairs Division, pp. 1\u201345","DOI":"10.1007\/978-3-642-79361-5_1"},{"key":"24_CR5","unstructured":"CoFI Language Design Task Group, CASL \u2013 The CoFI Algebraic Specification Language \u2013 Summary, version 1.0, 22 (July 1999), available at \n                      http:\/\/www.dcs.ed.ac.uk\/home\/dts\/CoFI\/Documents\/CASL\/Summary\/index.html"},{"key":"24_CR6","unstructured":"Cengarle, M. V., Formal Specifications with Higher-Order Parametrization, PhD Thesis, Ludwig-Maximilians-Universit\u00e4t, M\u00fcnchen (1994)"},{"key":"24_CR7","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986)"},{"key":"24_CR8","doi-asserted-by":"crossref","first-page":"222","DOI":"10.1007\/978-1-4612-0325-4_8","volume-title":"Logical Methods","author":"J.N. Crossley","year":"1993","unstructured":"Crossley, J.N., Shepherdson, J.C.: Extracting programs from proofs by an extension of the Curry-Howard process. In: Crossley, J.N., Remmel, J.B., Shore, R.A., Sweedler, M.E. (eds.) Logical Methods, pp. 222\u2013288. Birkh\u00e4user, Boston (1993)"},{"key":"24_CR9","unstructured":"Crossley, J.N., Poernomo, I.H., Wirsing, M.: Extracting Structured Programs from Specification Proofs (in preparation)"},{"key":"24_CR10","first-page":"249","volume":"110","author":"J. Gallier","year":"1993","unstructured":"Gallier, J.: Constructive Logics. A Tutorial on Proof-systems and Typed \u03bb-Calculi. TCS\u00a0110, 249\u2013339 (1993)","journal-title":"A Tutorial on Proof-systems and Typed \u03bb-Calculi, TCS"},{"key":"24_CR11","volume-title":"Proofs and types","author":"J.-Y. Girard","year":"1989","unstructured":"Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and types. Cambridge University Press, Cambridge (1989)"},{"key":"24_CR12","doi-asserted-by":"publisher","first-page":"27","DOI":"10.2307\/2964334","volume":"25","author":"R. Harrop","year":"1960","unstructured":"Harrop, R.: Concerning formulas of the types A \u2192 B\u2009\u2228\u2009C, A \u2192 (Ex)B(x) in Intuitionistic Formal Systems. J. Symb. Logic\u00a025, 27\u201332 (1960)","journal-title":"J. Symb. Logic"},{"key":"24_CR13","volume-title":"PX, a computational logic","author":"S. Hayashi","year":"1988","unstructured":"Hayashi, S., Nakano, H.: PX, a computational logic. MIT Press, Cambridge (1988)"},{"key":"24_CR14","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1016\/S0304-3975(96)00162-4","volume":"173","author":"R. Hennicker","year":"1997","unstructured":"Hennicker, R., Wirsing, M., Bidoit, M.: Proof systems for structured specifications with observability operators. TCS\u00a0173, 393\u2013443 (1997)","journal-title":"TCS"},{"key":"24_CR15","unstructured":"Jeavons, J., Poernomo, I., Crossley, J., Basit, B.: Fred: an implementation of a layered approach to extracting programs from proofs. Part I: an application in graph theory. In: Lloyd, J.W. (ed.) AWCL (Australian Workshop on Computational Logic), Proceedings, Canberra, Australia, pp. 57\u201366 (February 2000)"},{"key":"24_CR16","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)"},{"key":"24_CR17","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF00283329","volume":"25","author":"D.T. Sannella","year":"1988","unstructured":"Sannella, D.T., Tarlecki, A.: Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Informatica\u00a025, 233\u2013281 (1988)","journal-title":"Acta Informatica"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BFb0015464","volume-title":"KORSO: Methods, Languages, and Tools for the Construction of Correct Software, Final Report","author":"T. Santen","year":"1995","unstructured":"Santen, T., Kamm\u00fcller, F., J\u00e4hnichen, S., Beyer, M.: Formalization of Algebraic Specification in the Development language DEVA. In: J\u00e4hnichen, S., Broy, M. (eds.) KORSO 1995. LNCS, vol.\u00a01009, pp. 223\u2013238. Springer, Heidelberg (1995)"},{"key":"24_CR19","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1016\/S0747-7171(06)80006-4","volume":"15","author":"D.R. Smith","year":"1993","unstructured":"Smith, D.R.: Constructing Specification Morphisms. J. Symbolic Computation\u00a015, 571\u2013606 (1993)","journal-title":"J. Symbolic Computation"},{"key":"24_CR20","doi-asserted-by":"crossref","unstructured":"Wirsing, M. and M. Broy: A modular framework for algebraic specification and implementation, in J. Diaz and F. Orejas (eds), TAPSOFT 89, LNCS 351, vol. 1, Springer, 1989, pp. 42\u201373. 420","DOI":"10.1007\/3-540-50939-9_124"},{"key":"24_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/3-540-48483-3_21","volume-title":"Recent Trends in Algebraic Development Techniques","author":"M. Wirsing","year":"1999","unstructured":"Wirsing, M., Crossley, J.N., Peterreins, H.: Proof normalization of structured algebraic specifications is convergent. In: Fiadeiro, J.L. (ed.) WADT 1998. LNCS, vol.\u00a01589, pp. 326\u2013340. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-44616-3_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,18]],"date-time":"2023-02-18T03:41:13Z","timestamp":1676691673000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-540-44616-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678984","9783540446163"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-44616-3_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}