{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:11:21Z","timestamp":1725484281393},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540431596"},{"type":"electronic","value":"9783540456452"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45645-7_14","type":"book-chapter","created":{"date-parts":[[2007,5,29]],"date-time":"2007-05-29T02:24:22Z","timestamp":1180405462000},"page":"280-304","source":"Crossref","is-referenced-by-count":0,"title":["Programs, Proofs and Parametrized Specifications"],"prefix":"10.1007","author":[{"given":"Iman","family":"Poernomo","sequence":"first","affiliation":[]},{"given":"John N.","family":"Crossley","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Wirsing","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,1,29]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"U. Berger and H. Schwichtenberg, Program development by Proof Transformation, pp. 1\u201345 in Proceedings of the NATO Advanced Study Institute on Proof and Computation, Marktoberdorf, Germany, 1993.","DOI":"10.1007\/978-3-642-79361-5_1"},{"key":"14_CR2","unstructured":"M. V. Cengarle, Formal Specifications with higher-order parametrization. PhD thesis, Ludwig-Maximilians-Universit\u00e4t, Munich, 1995."},{"key":"14_CR3","unstructured":"CoFILanguage Design Task Group on Language Design, CASL, The Common Algebraic Specification Language, Summary, 25 March 2001, available at http:\/\/www.brics.dk\/Projects\/CoFI\/Documents\/CASL\/Summary\/ (accessed 28.05.2001)."},{"key":"14_CR4","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R. L. Constable","year":"1986","unstructured":"R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. Harper, D. J. Howe, T. B. Knoblock, N. P. Panangaden, J. T. Sasaki, and S. F. Smith, Implementing Mathematics with the Nuprl Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"issue":"1","key":"14_CR5","first-page":"71","volume":"7","author":"J. N. Crossley","year":"2001","unstructured":"J. N. Crossley and I. Poernomo, Fred: An approach to generating real, correct, reusable programs from proofs, FMTOOLS 2000, special issue of J.U.C.S., 7, no.1, 71\u201388, available at http:\/\/www.jucs.org\/jucs_7_1\/fred_an_approach_to (accessed 28.05.2001).","journal-title":"J.U.C.S."},{"key":"14_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"419","DOI":"10.1007\/978-3-540-44616-3_24","volume-title":"Recent Trends in Algebraic Development Techniques (WADT\u201999)","author":"J. N. Crossley","year":"2000","unstructured":"J. N. Crossley, I. Poernomo and M. Wirsing, Extraction of Structured Programs from Specification Proofs, pp. 419\u2013437 in D. Bert, C. Choppy and P. Mosses (eds), Recent Trends in Algebraic Development Techniques (WADT\u201999), Lecture Notes in Computer Science 1827, Berlin: Springer, 2000."},{"key":"14_CR7","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":"J. N. Crossley and J. C. Shepherdson, Extracting programs from proofs by an extension of the Curry-Howard process, pp. 222\u2013288 in J. N. Crossley, J. B. Remmel, R. A. Shore, and M. E. Sweedler (eds),Logical Methods, Birkh\u00e4user, Boston, 1993."},{"key":"14_CR8","unstructured":"J.-Y. Girard, Y. Lafont and P. Taylor, Proofs and types, Cambridge University Press, 1989."},{"key":"14_CR9","volume-title":"PX, a computational logic","author":"S. Hayashi","year":"1988","unstructured":"S. Hayashi and H. Nakano, PX, a computational logic. MIT Press, Cambridge, Mass., 1988."},{"key":"14_CR10","unstructured":"G. Huet, G. Kahn, and C. Paulin-Mohring. The Coq Proof assistant Reference Manual: Version 6.1. Coq project research report RT-0203, Inria, 1997."},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1016\/S0304-3975(96)00163-6","volume":"173","author":"S. Kahrs","year":"1997","unstructured":"S. Kahrs, D. Sannella and A. Tarlecki, The definition of Extended ML: A gentle introduction. Theoretical Computer Science, 173 (1997) 445\u2013484.","journal-title":"Theoretical Computer Science"},{"key":"14_CR12","volume-title":"Intuitionistic Type Theory","author":"P. Martin-L\u00f6f","year":"1984","unstructured":"Per Martin-L\u00f6f, Intuitionistic Type Theory, Bibliopolis, Naples, Italy, 1984."},{"key":"14_CR13","volume-title":"The definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"R. Milner, M. Tofte, and R. Harper, The definition of Standard ML. Cambridge, Mass., MIT Press, 1990."},{"key":"14_CR14","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/978-3-642-59851-7_6","volume-title":"Algebraic Foundations of Systems Specification","author":"F. Orejas","year":"1999","unstructured":"F. Orejas. Structuring and modularity, pp. 159\u2013200 in E. Astesiano, H.-J. Kreowski, B. Krieg-Bruckner (eds), Algebraic Foundations of Systems Specification, IFIP State-of-the-Art Reports. Berlin, Springer, 1999."},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"L. C. Paulson, ML for the Working Programmer, second edition. Cambridge University Press, 1996.","DOI":"10.1017\/CBO9780511811326"},{"key":"14_CR16","unstructured":"H. Peterreins, A natural-deduction-like calculus for structured Specifications. PhD thesis, Ludwig-Maximilians-Universit\u00e4t, Munich, 1996."},{"key":"14_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/3-540-50940-2_48","volume-title":"TAPSOFT\u2019 89","author":"D. Sannella","year":"1989","unstructured":"D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology, pp 375\u2013389 in J. Diaz and F. Orejas (eds), TAPSOFT\u2019 89, vol. 2, Lecture Notes in Computer Science 352, Berlin, Springer 1989."},{"key":"14_CR18","doi-asserted-by":"publisher","first-page":"571","DOI":"10.1016\/S0747-7171(06)80006-4","volume":"15","author":"D.R. Smith","year":"1993","unstructured":"D.R. Smith, Constructing Specification Morphisms, Journal of Symbolic Computation, 15 (1993) 571\u2013606","journal-title":"Journal of Symbolic Computation"},{"key":"14_CR19","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1016\/0304-3975(86)90051-4","volume":"43","author":"M. Wirsing","year":"1986","unstructured":"M. Wirsing, Structured algebraic Specifications: a kernel language, Theoretical Computer Science, 43 (1986) 123\u2013250.","journal-title":"Theoretical Computer Science"},{"key":"14_CR20","first-page":"675","volume-title":"Handbook of Theoretical Computer Science","author":"M. Wirsing","year":"1990","unstructured":"M. Wirsing, Algebraic Specification, pp.675\u2013788in J. van Leeuwen, (ed.), Handbook of Theoretical Computer Science, volume B, Amsterdam; New York: Elsevier; Cambridge, Mass.: MIT Press, 1990."},{"key":"14_CR21","series-title":"Lect Notes Comput Sci","first-page":"322","volume-title":"Proceedings of the Twelfth International Workshop on Recent Trends in Algebraic Development Techniques","author":"M. Wirsing","year":"1999","unstructured":"M. Wirsing, J. N. Crossley and H. Peterreins, Proof normalization of structured algebraic Specifications is convergent, pp. 322\u2013337 in J. Fiadeiro (ed.), Proceedings of the Twelfth International Workshop on Recent Trends in Algebraic Development Techniques, Lecture Notes in Computer Science 1589, Berlin, Springer, 1999."}],"container-title":["Lecture Notes in Computer Science","Recent Trends in Algebraic Development Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45645-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T11:39:10Z","timestamp":1556451550000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45645-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540431596","9783540456452"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-45645-7_14","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}