{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T07:48:19Z","timestamp":1742975299166,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642242755"},{"type":"electronic","value":"9783642242762"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24276-2_5","type":"book-chapter","created":{"date-parts":[[2011,10,10]],"date-time":"2011-10-10T10:49:23Z","timestamp":1318243763000},"page":"72-88","source":"Crossref","is-referenced-by-count":4,"title":["Automating Derivations of Abstract Machines from Reduction Semantics:"],"prefix":"10.1007","author":[{"given":"Filip","family":"Sieczkowski","sequence":"first","affiliation":[]},{"given":"Ma\u0142gorzata","family":"Biernacka","sequence":"additional","affiliation":[]},{"given":"Dariusz","family":"Biernacki","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","unstructured":"Biernacka, M., Biernacki, D.: Formalizing constructions of abstract machines for functional languages in Coq. In: Giesl, J. (ed.) Preliminary proceedings of the Seventh International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2007), Paris, France (June 2007)"},{"issue":"1","key":"5_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1297658.1297664","volume":"9","author":"M. Biernacka","year":"2007","unstructured":"Biernacka, M., Danvy, O.: A concrete framework for environment machines. ACM Transactions on Computational Logic\u00a09(1), 1\u201330 (2007)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"1-3","key":"5_CR3","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1016\/j.tcs.2006.12.028","volume":"375","author":"M. Biernacka","year":"2007","unstructured":"Biernacka, M., Danvy, O.: A syntactic correspondence between context-sensitive calculi and abstract machines. Theoretical Computer Science\u00a0375(1-3), 76\u2013108 (2007)","journal-title":"Theoretical Computer Science"},{"key":"5_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-642-04164-8_10","volume-title":"Semantics and Algebraic Specification","author":"M. Biernacka","year":"2009","unstructured":"Biernacka, M., Danvy, O.: Towards compatible and interderivable semantic specifications for the Scheme programming language, Part II: Reduction semantics and abstract machines. In: Palsberg, J. (ed.) Semantics and Algebraic Specification. LNCS, vol.\u00a05700, pp. 186\u2013206. Springer, Heidelberg (2009)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/10930755_18","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Chrz\u0105szcz","year":"2003","unstructured":"Chrz\u0105szcz, J.: Implementing modules in the Coq system. In: Basin, D.A., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 270\u2013286. Springer, Heidelberg (2003)"},{"key":"5_CR6","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1016\/0304-3975(91)90230-Y","volume":"82","author":"P.-L. Curien","year":"1991","unstructured":"Curien, P.-L.: An abstract framework for environment machines. Theoretical Computer Science\u00a082, 389\u2013402 (1991)","journal-title":"Theoretical Computer Science"},{"key":"5_CR7","series-title":"SIGPLAN Notices","volume-title":"Proceedings of the 2008 ACM SIGPLAN International Conference on Functional Programming (ICFP 2008)","author":"O. Danvy","year":"2008","unstructured":"Danvy, O.: Defunctionalized interpreters for programming languages. In: Thiemann, P. (ed.) Proceedings of the 2008 ACM SIGPLAN International Conference on Functional Programming (ICFP 2008), Victoria, British Columbia. SIGPLAN Notices, vol.\u00a043(9), ACM Press, New York (September 2008)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-642-04652-0_3","volume-title":"Advanced Functional Programming","author":"O. Danvy","year":"2009","unstructured":"Danvy, O.: From reduction-based to reduction-free normalization. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol.\u00a05832, pp. 66\u2013164. Springer, Heidelberg (2009)"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1016\/j.jcss.2009.10.004","volume":"76","author":"O. Danvy","year":"2010","unstructured":"Danvy, O., Johannsen, J.: Inter-deriving semantic artifacts for object-oriented programming. Journal of Computer and System Sciences\u00a076, 302\u2013323 (2010)","journal-title":"Journal of Computer and System Sciences"},{"issue":"3","key":"5_CR10","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1016\/j.ipl.2007.10.010","volume":"106","author":"O. Danvy","year":"2008","unstructured":"Danvy, O., Millikin, K.: On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion. Information Processing Letters\u00a0106(3), 100\u2013109 (2008)","journal-title":"Information Processing Letters"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"240","DOI":"10.1007\/978-3-642-12251-4_18","volume-title":"Functional and Logic Programming","author":"O. Danvy","year":"2010","unstructured":"Danvy, O., Millikin, K., Munk, J., Zerny, I.: Defunctionalized interpreters for call-by-need evaluation. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol.\u00a06009, pp. 240\u2013256. Springer, Heidelberg (2010)"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. Research Report BRICS RS-04-26, DAIMI, Department of Computer Science, Aarhus University, Aarhus, Denmark, A preliminary version appeared in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001). Electronic Notes in Theoretical Computer Science, Vol.\u00a059(4) (November 2004)","DOI":"10.7146\/brics.v11i26.21851"},{"key":"5_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-20551-4_1","volume-title":"Logic-Based Program Synthesis and Transformation","author":"O. Danvy","year":"2011","unstructured":"Danvy, O., Zerny, I.: Three syntactic theories for combinatory graph reduction. In: Alpuente, M. (ed.) LOPSTR 2010. LNCS, vol.\u00a06564, pp. 1\u201320. Springer, Heidelberg (2011)"},{"key":"5_CR14","volume-title":"Proceedings of the 2011 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2011)","author":"O. Danvy","year":"2011","unstructured":"Danvy, O., Zerny, I., Johannsen, J.: A walk in the semantic park. In: Proceedings of the 2011 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM 2011), Austin, USA. ACM Press, New York (January 2011) Invited talk"},{"key":"5_CR15","first-page":"193","volume-title":"Formal Description of Programming Concepts III","author":"M. Felleisen","year":"1986","unstructured":"Felleisen, M., Friedman, D.P.: Control operators, the SECD machine, and the \u03bb-calculus. In: Wirsing, M. (ed.) Formal Description of Programming Concepts III, pp. 193\u2013217. Elsevier Science Publishers B.V., North-Holland (1986)"},{"issue":"3:1","key":"5_CR16","first-page":"1","volume":"6","author":"R. Garcia","year":"2010","unstructured":"Garcia, R., Lumsdaine, A., Sabry, A.: Lazy evaluation and delimited control. Logical Methods in Computer Science\u00a06(3:1), 1\u201339 (2010)","journal-title":"Logical Methods in Computer Science"},{"issue":"3","key":"5_CR17","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s10990-007-9018-9","volume":"20","author":"J.-L. Krivine","year":"2007","unstructured":"Krivine, J.-L.: A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation\u00a020(3), 199\u2013207 (2007)","journal-title":"Higher-Order and Symbolic Computation"}],"container-title":["Lecture Notes in Computer Science","Implementation and Application of Functional Languages"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24276-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T11:35:01Z","timestamp":1578483301000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24276-2_5"}},"subtitle":["A Generic Formalization of Refocusing in Coq"],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642242755","9783642242762"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24276-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}