{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:42:29Z","timestamp":1767926549223,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T00:00:00Z","timestamp":1663632000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,9,20]]},"DOI":"10.1145\/3551357.3551384","type":"proceedings-article","created":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T15:37:25Z","timestamp":1663688245000},"page":"1-48","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Certified Derivation of Small-Step From Big-Step Skeletal Semantics"],"prefix":"10.1145","author":[{"given":"Guillaume","family":"Ambal","sequence":"first","affiliation":[{"name":"Univ Rennes, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sergue\u00ef","family":"Lenglet","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Lorraine, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alan","family":"Schmitt","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Camille","family":"No\u00fbS","sequence":"additional","affiliation":[{"name":"Laboratoire Cogitamus, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,9,20]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2021. ECMAScript language specification. Standard ECMA-262. https:\/\/262.ecma-international.org\/  2021. ECMAScript language specification. Standard ECMA-262. https:\/\/262.ecma-international.org\/"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888254"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503676"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Guillaume Ambal Sergue\u00ef Lenglet and Alan Schmitt. 2022. Certified Derivation of Small-Step From Big-Step Skeletal Semantics. Implementation available at https:\/\/gitlab.inria.fr\/skeletons\/necro\/-\/tree\/PPDP2022.  Guillaume Ambal Sergue\u00ef Lenglet and Alan Schmitt. 2022. Certified Derivation of Small-Step From Big-Step Skeletal Semantics. Implementation available at https:\/\/gitlab.inria.fr\/skeletons\/necro\/-\/tree\/PPDP2022.","DOI":"10.1145\/3551357.3551384"},{"key":"e_1_3_2_1_5_1","volume-title":"POPL","author":"Bodin Martin","year":"2019","unstructured":"Martin Bodin , Philippa Gardner , Thomas Jensen , and Alan Schmitt . 2019. Skeletal semantics and their interpretations. PACMPL 3 , POPL ( 2019 ), 44:1\u201344:31. https:\/\/doi.org\/10.1145\/3290357 10.1145\/3290357 Martin Bodin, Philippa Gardner, Thomas Jensen, and Alan Schmitt. 2019. Skeletal semantics and their interpretations. PACMPL 3, POPL (2019), 44:1\u201344:31. https:\/\/doi.org\/10.1145\/3290357"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_3"},{"key":"e_1_3_2_1_7_1","volume-title":"10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings(Lecture Notes in Computer Science, Vol.\u00a07940)","author":"Ciob\u00e2c\u0103 \u015etefan","year":"2013","unstructured":"\u015etefan Ciob\u00e2c\u0103 . 2013 . From Small-Step Semantics to Big-Step Semantics, Automatically. In Integrated Formal Methods , 10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings(Lecture Notes in Computer Science, Vol.\u00a07940) , Einar\u00a0Broch Johnsen and Luigia Petre (Eds.). Springer, 347\u2013361. https:\/\/doi.org\/10.1007\/978-3-642-38613-8_24 10.1007\/978-3-642-38613-8_24 \u015etefan Ciob\u00e2c\u0103. 2013. From Small-Step Semantics to Big-Step Semantics, Automatically. In Integrated Formal Methods, 10th International Conference, IFM 2013, Turku, Finland, June 10-14, 2013. Proceedings(Lecture Notes in Computer Science, Vol.\u00a07940), Einar\u00a0Broch Johnsen and Luigia Petre (Eds.). Springer, 347\u2013361. https:\/\/doi.org\/10.1007\/978-3-642-38613-8_24"},{"key":"e_1_3_2_1_8_1","unstructured":"The Coq Development\u00a0Team. 2020. The Coq Proof Assistant Reference Manual version 8.11. http:\/\/coq.inria.fr  The Coq Development\u00a0Team. 2020. The Coq Proof Assistant Reference Manual version 8.11. http:\/\/coq.inria.fr"},{"key":"e_1_3_2_1_9_1","volume-title":"Necro: Animating Skeletons. In ML","author":"Courant Nathana\u00ebl","year":"2019","unstructured":"Nathana\u00ebl Courant , Enzo Crance , and Alan Schmitt . 2019 . Necro: Animating Skeletons. In ML 2019. Berlin, Germany. Nathana\u00ebl Courant, Enzo Crance, and Alan Schmitt. 2019. Necro: Animating Skeletons. In ML 2019. Berlin, Germany."},{"key":"e_1_3_2_1_10_1","volume-title":"16th International Workshop, IFL 2004","author":"Danvy Olivier","year":"2004","unstructured":"Olivier Danvy . 2004 . A Rational Deconstruction of Landin\u2019s SECD Machine. In Implementation and Application of Functional Languages , 16th International Workshop, IFL 2004 , L\u00fcbeck, Germany , September 8-10, 2004, Revised Selected Papers(Lecture Notes in Computer Science, Vol.\u00a03474), Clemens Grelck, Frank Huch, Greg Michaelson, and Philip\u00a0W. Trinder (Eds.). Springer, 52\u201371. https:\/\/doi.org\/10.1007\/11431664_4 10.1007\/11431664_4 Olivier Danvy. 2004. A Rational Deconstruction of Landin\u2019s SECD Machine. In Implementation and Application of Functional Languages, 16th International Workshop, IFL 2004, L\u00fcbeck, Germany, September 8-10, 2004, Revised Selected Papers(Lecture Notes in Computer Science, Vol.\u00a03474), Clemens Grelck, Frank Huch, Greg Michaelson, and Philip\u00a0W. Trinder (Eds.). Springer, 52\u201371. https:\/\/doi.org\/10.1007\/11431664_4"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.01.007"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1929501.1929503"},{"key":"e_1_3_2_1_13_1","volume-title":"Concurrency, Compositionality, and Correctness, Essays in Honor of Willem-Paul de Roever(Lecture Notes in Computer Science, Vol.\u00a05930)","author":"Huizing Cornelis","unstructured":"Cornelis Huizing , Ron Koymans , and Ruurd Kuiper . 2010. A Small Step for Mankind . In Concurrency, Compositionality, and Correctness, Essays in Honor of Willem-Paul de Roever(Lecture Notes in Computer Science, Vol.\u00a05930) , Dennis Dams, Ulrich Hannemann, and Martin Steffen (Eds.). Springer , 66\u201373. https:\/\/doi.org\/10.1007\/978-3-642-11512-7_5 10.1007\/978-3-642-11512-7_5 Cornelis Huizing, Ron Koymans, and Ruurd Kuiper. 2010. A Small Step for Mankind. In Concurrency, Compositionality, and Correctness, Essays in Honor of Willem-Paul de Roever(Lecture Notes in Computer Science, Vol.\u00a05930), Dennis Dams, Ulrich Hannemann, and Martin Steffen (Eds.). Springer, 66\u201373. https:\/\/doi.org\/10.1007\/978-3-642-11512-7_5"},{"key":"e_1_3_2_1_14_1","volume-title":"4th Annual Symposium on Theoretical Aspects of Computer Science","author":"Kahn Gilles","year":"1987","unstructured":"Gilles Kahn . 1987 . Natural Semantics. In STACS 87 , 4th Annual Symposium on Theoretical Aspects of Computer Science , Passau, Germany , February 19-21, 1987, Proceedings(Lecture Notes in Computer Science, Vol.\u00a0247), Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing (Eds.). Springer, 22\u201339. https:\/\/doi.org\/10.1007\/BFb0039592 10.1007\/BFb0039592 Gilles Kahn. 1987. Natural Semantics. In STACS 87, 4th Annual Symposium on Theoretical Aspects of Computer Science, Passau, Germany, February 19-21, 1987, Proceedings(Lecture Notes in Computer Science, Vol.\u00a0247), Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing (Eds.). Springer, 22\u201339. https:\/\/doi.org\/10.1007\/BFb0039592"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_17_1","unstructured":"Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2020. The OCaml system release 4.10. Inria. https:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/  Xavier Leroy Damien Doligez Alain Frisch Jacques Garrigue Didier R\u00e9my and J\u00e9r\u00f4me Vouillon. 2020. The OCaml system release 4.10. Inria. https:\/\/caml.inria.fr\/pub\/docs\/manual-ocaml\/"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2007.12.004"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","unstructured":"Robin Milner Robert Harper David MacQueen and Tofte Mads. 1997. The Definition of Standard ML Revised Edition.  Robin Milner Robert Harper David MacQueen and Tofte Mads. 1997. The Definition of Standard ML Revised Edition.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_3_2_1_21_1","volume-title":"Semantics with applications - a formal introduction","author":"Nielson Hanne\u00a0Riis","unstructured":"Hanne\u00a0Riis Nielson and Flemming Nielson . 1992. Semantics with applications - a formal introduction . Wiley . Hanne\u00a0Riis Nielson and Flemming Nielson. 1992. Semantics with applications - a formal introduction. Wiley."},{"key":"e_1_3_2_1_22_1","volume-title":"A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61","author":"Plotkin D.","year":"2004","unstructured":"Gordon\u00a0 D. Plotkin . 2004. A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61 ( 2004 ), 17\u2013139. Gordon\u00a0D. Plotkin. 2004. A structural approach to operational semantics. Journal of Logic and Algebraic Programming 60-61 (2004), 17\u2013139."},{"key":"e_1_3_2_1_23_1","volume-title":"ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings(Lecture Notes in Computer Science, Vol.\u00a08410)","author":"Poulsen Casper\u00a0Bach","year":"2014","unstructured":"Casper\u00a0Bach Poulsen and Peter\u00a0 D. Mosses . 2014 . Deriving Pretty-Big-Step Semantics from Small-Step Semantics. In Programming Languages and Systems - 23rd European Symposium on Programming , ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings(Lecture Notes in Computer Science, Vol.\u00a08410) , Zhong Shao (Ed.). Springer, 270\u2013289. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_15 10.1007\/978-3-642-54833-8_15 Casper\u00a0Bach Poulsen and Peter\u00a0D. Mosses. 2014. Deriving Pretty-Big-Step Semantics from Small-Step Semantics. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings(Lecture Notes in Computer Science, Vol.\u00a08410), Zhong Shao (Ed.). Springer, 270\u2013289. https:\/\/doi.org\/10.1007\/978-3-642-54833-8_15"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2016.05.001"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.05.003"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_3_2_1_27_1","volume-title":"Programming Languages and Systems - 28th European Symposium on Programming, ESOP","author":"Vesely Ferdinand","year":"2019","unstructured":"Ferdinand Vesely and Kathleen Fisher . 2019. One Step at a Time - A Functional Derivation of Small-Step Evaluators from Big-Step Counterparts . In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019 , Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings(Lecture Notes in Computer Science, Vol.\u00a011423), Lu\u00eds Caires (Ed.). Springer , 205\u2013231. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_8 10.1007\/978-3-030-17184-1_8 Ferdinand Vesely and Kathleen Fisher. 2019. One Step at a Time - A Functional Derivation of Small-Step Evaluators from Big-Step Counterparts. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings(Lecture Notes in Computer Science, Vol.\u00a011423), Lu\u00eds Caires (Ed.). Springer, 205\u2013231. https:\/\/doi.org\/10.1007\/978-3-030-17184-1_8"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"event":{"name":"PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming","location":"Tbilisi Georgia","acronym":"PPDP 2022"},"container-title":["Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551357.3551384","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3551357.3551384","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:24Z","timestamp":1750186824000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551357.3551384"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,20]]},"references-count":28,"alternative-id":["10.1145\/3551357.3551384","10.1145\/3551357"],"URL":"https:\/\/doi.org\/10.1145\/3551357.3551384","relation":{},"subject":[],"published":{"date-parts":[[2022,9,20]]},"assertion":[{"value":"2022-09-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}