{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T02:10:31Z","timestamp":1737339031218,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540421276"},{"type":"electronic","value":"9783540451426"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45142-0_2","type":"book-chapter","created":{"date-parts":[[2007,8,1]],"date-time":"2007-08-01T01:17:34Z","timestamp":1185931054000},"page":"18-37","source":"Crossref","is-referenced-by-count":1,"title":["Protocols between Programs and Proofs"],"prefix":"10.1007","author":[{"given":"Iman","family":"Poernomo","sequence":"first","affiliation":[]},{"given":"John N.","family":"Crossley","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,5,2]]},"reference":[{"key":"2_CR1","unstructured":"David Albrecht and John N. Crossley. Program extraction, simplified proof-terms and realizability. Technical Report 96\/275, Department of Computer Science, Monash University, 1996."},{"key":"2_CR2","unstructured":"Penny Anderson. Program Derivation by Proof Transformation. PhD thesis, Carnegie Mellon University, 1993."},{"key":"2_CR3","doi-asserted-by":"crossref","unstructured":"Ulrich Berger and Helmut Schwichtenberg, Program development by Proof Transformation. Pp. 1\u201345 in Proceedings of the NATO Advanced Study Institute on Proof and Computation, Marktoberdorf, Germany, 1993, published in cooperation with the NATO Scientific Affairs Division.","DOI":"10.1007\/978-3-642-79361-5_1"},{"key":"2_CR4","doi-asserted-by":"crossref","unstructured":"James L. Caldwell. Moving Proofs-As-Programs into Practice. Pp. 10\u201317 in Proceedings 12th IEEE International Conference Automated Software Engineering, IEEE Computer Society, 1998.","DOI":"10.1109\/ASE.1997.632819"},{"key":"2_CR5","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/978-3-642-59048-1_4","volume-title":"Logic of computation (Marktoberdorf, 1995)","author":"R. L. Constable","year":"1997","unstructured":"Robert L. Constable. The structure of Nuprl\u2019s type theory. Pp. 123\u2013155 in H. Schwichtenberg, editor, Logic of computation (Marktoberdorf, 1995), NATO Adv. Sci. Inst. Ser. F Comput. Systems Sci., 157, Springer, Berlin, 1997."},{"key":"2_CR6","volume-title":"Implementing Mathematics with the Nuprl Development System","author":"R. L. Constable","year":"1986","unstructured":"Robert 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."},{"key":"2_CR7","doi-asserted-by":"crossref","unstructured":"John N. Crossley and John C. Shepherdson. Extracting programs from proofs by an extension of the Curry-Howard process. Pp. 222\u2013288 in John N. Crossley, J. B. Remmel, R. Shore, and M. Sweedler, editors. Logical Methods: Essays in honor of A. Nerode. Birkh\u00e4user, Boston, Mass., 1993.","DOI":"10.1007\/978-1-4612-0325-4_8"},{"key":"2_CR8","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":"John N. Crossley, Iman 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":"2_CR9","volume-title":"PX, a computational logic","author":"S. Hayashi","year":"1988","unstructured":"Susumu Hayashi and Hiroshi Nakano. PX, a computational logic. MIT Press, Cambridge, Mass., 1988."},{"key":"2_CR10","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L. Henkin","year":"1950","unstructured":"Leon Henkin. Completeness in the Theory of Types. Journal of Symbolic Logic, 15 (1950) 81\u201391.","journal-title":"Journal of Symbolic Logic"},{"key":"2_CR11","first-page":"479","volume-title":"To H.B. Curry: essays on combinatory logic, lambda calculus, and formalism","author":"W. A. Howard","year":"1980","unstructured":"William A. Howard. The formulae-as-types notion of construction. Pp. 479\u2013490 in John R. Seldin and R. J. Hindley, editors, To H.B. Curry: essays on combinatory logic, lambda calculus, and formalism. Academic Press, London, New York, 1980."},{"key":"2_CR12","unstructured":"Gerard 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":"2_CR13","unstructured":"John S. Jeavons, I. Poernomo, B. Basit and J. N. Crossley. A layered approach to extracting programs from proofs with an application in Graph Theory. Paper presented at the Seventh Asian Logic Conference, Hsi-Tou, Taiwan, June 1999. Available as T. R. 2000\/55, School of Computer Science and Software Engineering, Monash University, Melbourne, Australia."},{"key":"2_CR14","unstructured":"John S. Jeavons, I. Poernomo, J. N. Crossley and B. Basit. Fred: An implementation of a layered approach to extracting programs from proofs. Part I: an application in Graph Theory. AWCL (Australian Workshop on Computational Logic), Proceedings, Canberra, Australia, February 2000, pp. 57\u201366."},{"key":"2_CR15","unstructured":"Zhaohui Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994."},{"key":"2_CR16","unstructured":"Per Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"2_CR17","unstructured":"Iman Poernomo. PhD thesis, School of Computer Science and Software Engineering, Monash University, in preparation."}],"container-title":["Lecture Notes in Computer Science","Logic Based Program Synthesis and Transformation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45142-0_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T01:32:08Z","timestamp":1737336728000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45142-0_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421276","9783540451426"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45142-0_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}