{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:45:53Z","timestamp":1767926753276,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662494974","type":"print"},{"value":"9783662494981","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49498-1_23","type":"book-chapter","created":{"date-parts":[[2016,3,21]],"date-time":"2016-03-21T09:36:06Z","timestamp":1458552966000},"page":"589-615","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":44,"title":["Functional Big-Step Semantics"],"prefix":"10.1007","author":[{"given":"Scott","family":"Owens","sequence":"first","affiliation":[]},{"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[]},{"given":"Ramana","family":"Kumar","sequence":"additional","affiliation":[]},{"given":"Yong Kiam","family":"Tan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/11693024_6","volume-title":"Programming Languages and Systems","author":"A Ahmed","year":"2006","unstructured":"Ahmed, A.: Step-indexed syntactic logical relations for recursive and quantified types. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 69\u201383. Springer, Heidelberg (2006). doi:\n                    10.1007\/11693024_6"},{"issue":"5","key":"23_CR2","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1145\/504709.504712","volume":"23","author":"AW Appel","year":"2001","unstructured":"Appel, A.W., McAllester, D.A.: An indexed model of recursive types for foundational proof-carrying code. ACM Trans. Program. Lang. Syst. 23(5), 657\u2013683 (2001). doi:\n                    10.1145\/504709.504712","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-642-54833-8_15","volume-title":"Programming Languages and Systems","author":"C Bach Poulsen","year":"2014","unstructured":"Bach Poulsen, C., Mosses, P.D.: Deriving pretty-big-step semantics from small-step semantics. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 270\u2013289. Springer, Heidelberg (2014). doi:\n                    10.1007\/978-3-642-54833-8_15"},{"key":"23_CR4","unstructured":"Poulsen, C.B., Mosses, P.D.: Divergence as state in coinductive big-step semantics (extended abstract). In: 26th Nordic Workshop on Programming Theory, NWPT 2014 (2014). \n                    http:\/\/www.plancomps.org\/nwpt2014\/"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-03359-9_11","volume-title":"Theorem Proving in Higher Order Logics","author":"S Berghofer","year":"2009","unstructured":"Berghofer, S., Bulwahn, L., Haftmann, F.: Turning inductive into equational specifications. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 131\u2013146. Springer, Heidelberg (2009). doi:\n                    10.1007\/978-3-642-03359-9_11"},{"issue":"3","key":"23_CR6","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning 43(3), 263\u2013288 (2009). doi:\n                    10.1007\/s10817-009-9148-3","journal-title":"J. Autom. Reasoning"},{"key":"23_CR7","doi-asserted-by":"publisher","unstructured":"Bodin, M., Chargu\u00e9raud, A., Filaretti, D., Gardner, P., Maffeis, S., Naudziuniene, D., Schmitt, A., Smith, G.: A trusted mechanised JavaScript specification. In: The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 87\u2013100 (2014). doi:\n                    10.1145\/2535838.2535876","DOI":"10.1145\/2535838.2535876"},{"key":"23_CR8","unstructured":"Boyer, R., Moore, J.S.: Mechanized formal reasoning about programs and computing machines. In: Automated Reasoning and Its Applications: Essays in Honor of Larry Wos. MIT Press (1996)"},{"key":"23_CR9","unstructured":"Chambart, P.: High level OCaml optimisations (2013). \n                    https:\/\/ocaml.org\/meetings\/ocaml\/2013\/slides\/chambart.pdf"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-37036-6_3","volume-title":"Programming Languages and Systems","author":"A Chargu\u00e9raud","year":"2013","unstructured":"Chargu\u00e9raud, A.: Pretty-big-step semantics. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 41\u201360. Springer, Heidelberg (2013). doi:\n                    10.1007\/978-3-642-37036-6_3"},{"key":"23_CR11","doi-asserted-by":"publisher","unstructured":"Danielsson, N.A.: Operational semantics using the partiality monad. In: ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, pp. 127\u2013138 (2012). doi:\n                    10.1145\/2364527.2364546","DOI":"10.1145\/2364527.2364546"},{"issue":"4\u20135","key":"23_CR12","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1017\/S095679681200024X","volume":"22","author":"D Dreyer","year":"2012","unstructured":"Dreyer, D., Neis, G., Birkedal, L.: The impact of higher-order state and control effects on local relational reasoning. J. Funct. Program. 22(4\u20135), 477\u2013528 (2012). doi:\n                    10.1017\/S095679681200024X","journal-title":"J. Funct. Program."},{"key":"23_CR13","doi-asserted-by":"publisher","unstructured":"Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POpPL 2012, pp. 533\u2013544 (2012). doi:\n                    10.1145\/2103656.2103719","DOI":"10.1145\/2103656.2103719"},{"key":"23_CR14","doi-asserted-by":"publisher","unstructured":"Klein, C., Clements, J., Dimoulas, C., Eastlund, C., Felleisen, M., Flatt, M., McCarthy, J.A., Rafkind, J., Tobin-Hochstadt, S., Findler, R.B.: Run your research: on the effectiveness of lightweight mechanization. In: Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POpPL 2012, pp. 285\u2013296 (2012). doi:\n                    10.1145\/2103656.2103691","DOI":"10.1145\/2103656.2103691"},{"key":"23_CR15","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, pp. 179\u2013191. ACM Press (2014). doi:\n                    10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"23_CR16","doi-asserted-by":"publisher","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POpPL 2006, pp. 42\u201354 (2006). doi:\n                    10.1145\/1111037.1111042","DOI":"10.1145\/1111037.1111042"},{"issue":"4","key":"23_CR17","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reasoning 43(4), 363\u2013446 (2009). doi:\n                    10.1007\/s10817-009-9155-4","journal-title":"J. Autom. Reasoning"},{"issue":"2","key":"23_CR18","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1016\/j.ic.2007.12.004","volume":"207","author":"X Leroy","year":"2009","unstructured":"Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284\u2013304 (2009). doi:\n                    10.1016\/j.ic.2007.12.004","journal-title":"Inf. Comput."},{"key":"23_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-49519-3_22","volume-title":"Formal Methods in Computer-Aided Design","author":"JS Moore","year":"1998","unstructured":"Moore, J.S.: Symbolic simulation: an ACL2 approach. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol. 1522, pp. 334\u2013350. Springer, Heidelberg (1998). doi:\n                    10.1007\/3-540-49519-3_22"},{"key":"23_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/978-3-642-03359-9_26","volume-title":"Theorem Proving in Higher Order Logics","author":"K Nakata","year":"2009","unstructured":"Nakata, K., Uustalu, T.: Trace-based coinductive operational semantics for while. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 375\u2013390. Springer, Heidelberg (2009). doi:\n                    10.1007\/978-3-642-03359-9_26"},{"key":"23_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: With Isabelle\/HOL. Springer, Heidelberg (2014). doi:\n                    10.1007\/978-3-319-10542-0"},{"key":"23_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-78739-6_1","volume-title":"Programming Languages and Systems","author":"S Owens","year":"2008","unstructured":"Owens, S.: A sound semantics for OCaml light. In: Drossopoulou, S. (ed.) Programming Languages and Systems. Lecture Notes in Computer Science, vol. 4960, pp. 1\u201315. Springer, Heidelberg (2008). doi:\n                    10.1007\/978-3-540-78739-6_1"},{"issue":"4","key":"23_CR23","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1023\/A:1010027404223","volume":"11","author":"JC Reynolds","year":"1998","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. Higher-order and Symbolic Comput. 11(4), 363\u2013397 (1998). doi:\n                    10.1023\/A:1010027404223","journal-title":"Higher-order and Symbolic Comput."},{"key":"23_CR24","unstructured":"Rompf, T., Amin, N.: From F to DOT: type soundness proofs with definitional interpreters (2015). CoRR \n                    abs\/1510.05216"},{"key":"23_CR25","unstructured":"Siek, J.: Big-step, diverging or stuck? (2012). \n                    http:\/\/siek.blogspot.com\/2012\/07\/big-step-diverging-or-stuck.html"},{"key":"23_CR26","unstructured":"Siek, J.: Type safety in three easy lemmas (2013). \n                    http:\/\/siek.blogspot.com\/2013\/05\/type-safety-in-three-easy-lemmas.html"},{"issue":"1","key":"23_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(90)90018-D","volume":"89","author":"M Tofte","year":"1990","unstructured":"Tofte, M.: Type inference for polymorphic references. Inf. Comput. 89(1), 1\u201334 (1990). doi:\n                    10.1016\/0890-5401(90)90018-D","journal-title":"Inf. Comput."},{"key":"23_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-35308-6_9","volume-title":"Certified Programs and Proofs","author":"P-N Tollitte","year":"2012","unstructured":"Tollitte, P.-N., Delahaye, D., Dubois, C.: Producing certified functional code from inductive specifications. In: Hawblitzel, C., Miller, D. (eds.) CPP 2012. LNCS, vol. 7679, pp. 76\u201391. Springer, Heidelberg (2012). doi:\n                    10.1007\/978-3-642-35308-6_9"},{"issue":"1","key":"23_CR29","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"AK Wright","year":"1994","unstructured":"Wright, A.K., Felleisen, M.: A syntactic approach to type soundness. Inf. Comput. 115(1), 38\u201394 (1994). doi:\n                    10.1006\/inco.1994.1093","journal-title":"Inf. Comput."},{"issue":"4","key":"23_CR30","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/BF00243134","volume":"5","author":"WD Young","year":"1989","unstructured":"Young, W.D.: A mechanically verified code generator. J. Autom. Reasoning 5(4), 493\u2013518 (1989). doi:\n                    10.1007\/BF00243134","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49498-1_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,22]],"date-time":"2020-03-22T21:05:10Z","timestamp":1584911110000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49498-1_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662494974","9783662494981"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49498-1_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}