{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:25:21Z","timestamp":1770287121032,"version":"3.49.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T00:00:00Z","timestamp":1667174400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["VI.Veni.192.259"],"award-info":[{"award-number":["VI.Veni.192.259"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,10,31]]},"abstract":"<jats:p>\n            Specifying and mechanically verifying type safe programming languages requires significant effort. This effort can in theory be reduced by defining and reusing pre-verified, modular components. In practice, however, existing approaches to modular mechanical verification require many times as much specification code as plain, monolithic definitions. This makes it hard to develop new reusable components, and makes existing component specifications hard to grasp. We present an alternative approach based on intrinsically-typed interpreters, which reduces the size and complexity of modular specifications as compared to existing approaches. Furthermore, we introduce a new abstraction for safe-by-construction specification and composition of pre-verified type safe language components:\n            <jats:italic>language fragments<\/jats:italic>\n            . Language fragments are about as concise and easy to develop as plain, monolithic intrinsically-typed interpreters, but require about 10 times less code than previous approaches to modular mechanical verification of type safety.\n          <\/jats:p>","DOI":"10.1145\/3563355","type":"journal-article","created":{"date-parts":[[2022,10,31]],"date-time":"2022-10-31T20:23:35Z","timestamp":1667247815000},"page":"1903-1932","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Intrinsically-typed definitional interpreters \u00e0 la carte"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0059-5353","authenticated-orcid":false,"given":"Cas","family":"van der Rest","sequence":"first","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0622-7639","authenticated-orcid":false,"given":"Casper Bach","family":"Poulsen","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4789-9995","authenticated-orcid":false,"given":"Arjen","family":"Rouvoet","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7384-3370","authenticated-orcid":false,"given":"Eelco","family":"Visser","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5826-7520","authenticated-orcid":false,"given":"Peter","family":"Mosses","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,10,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029818"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236785"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681500009X"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009866"},{"key":"e_1_2_1_7_1","volume-title":"In Workshop on Dependent Types in Programming, Gothenburg.","author":"Augustsson Lennart","year":"1999","unstructured":"Lennart Augustsson and Magnus Carlsson . 1999 . An exercise in dependent types: A well-typed interpreter . In In Workshop on Dependent Types in Programming, Gothenburg. Lennart Augustsson and Magnus Carlsson. 1999. An exercise in dependent types: A well-typed interpreter. In In Workshop on Dependent Types in Programming, Gothenburg."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158104"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.76.3"},{"key":"e_1_2_1_10_1","volume-title":"Casper Bach Poulsen, and Nicolas Wu","author":"van den Berg Birthe","year":"2021","unstructured":"Birthe van den Berg , Tom Schrijvers , Casper Bach Poulsen, and Nicolas Wu . 2021 . Latent Effects for Reusable Language Components: Extended Version . CoRR abs\/2108.11155 (2021). arxiv:2108.11155 https:\/\/arxiv.org\/abs\/2108.11155 Birthe van den Berg, Tom Schrijvers, Casper Bach Poulsen, and Nicolas Wu. 2021. Latent Effects for Reusable Language Components: Extended Version. CoRR abs\/2108.11155 (2021). arxiv:2108.11155 https:\/\/arxiv.org\/abs\/2108.11155"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46734-3_4"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3426425.3426936"},{"key":"e_1_2_1_17_1","unstructured":"Jesper Cockx. 2017. Dependent Pattern Matching and Proof-Relevant Unification. (2017). https:\/\/lirias.kuleuven.be\/handle\/123456789\/583556 \t\t\t\t  Jesper Cockx. 2017. Dependent Pattern Matching and Proof-Relevant Unification. (2017). https:\/\/lirias.kuleuven.be\/handle\/123456789\/583556"},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the Workshop on Types for Proofs and Programs. Citeseer, 71\u201383","author":"Coquand Thierry","year":"1992","unstructured":"Thierry Coquand . 1992 . Pattern matching with dependent types . In Proceedings of the Workshop on Types for Proofs and Programs. Citeseer, 71\u201383 . Thierry Coquand. 1992. Pattern matching with dependent types. In Proceedings of the Workshop on Types for Proofs and Programs. Citeseer, 71\u201383."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_2"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000356"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796814000069"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429094"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500587"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034796"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(94)90120-1"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2502488.2502491"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503791"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000307"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19630090502"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199528"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.62.2"},{"key":"e_1_2_1_34_1","volume-title":"Unpublished manuscript","author":"McBride Conor","year":"2011","unstructured":"Conor McBride . 2011. Ornamental Algebras , Algebraic Ornaments . ( 2011 ). Unpublished manuscript . Conor McBride. 2011. Ornamental Algebras, Algebraic Ornaments. (2011). Unpublished manuscript."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211391"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.008"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04652-0_5"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3337932.3338813"},{"key":"e_1_2_1_44_1","volume-title":"Types and programming languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and programming languages . MIT Press . isbn:978-0-262-16209-8 Benjamin C. Pierce. 2002. Types and programming languages. MIT Press. isbn:978-0-262-16209-8"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7074690"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2428116.2428120"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.191.13"},{"key":"e_1_2_1_49_1","volume-title":"Siek","author":"Wadler Philip","year":"2020","unstructured":"Philip Wadler , Wen Kokke , and Jeremy G . Siek . 2020 . Programming Language Foundations in Agda . http:\/\/plfa.inf.ed.ac.uk\/20.07\/ Philip Wadler, Wen Kokke, and Jeremy G. Siek. 2020. Programming Language Foundations in Agda. http:\/\/plfa.inf.ed.ac.uk\/20.07\/"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473572"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563355","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3563355","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:02:33Z","timestamp":1750186953000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3563355"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,10,31]]},"references-count":50,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2022,10,31]]}},"alternative-id":["10.1145\/3563355"],"URL":"https:\/\/doi.org\/10.1145\/3563355","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,10,31]]},"assertion":[{"value":"2022-10-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}