{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,18]],"date-time":"2026-08-18T13:47:59Z","timestamp":1787060879470,"version":"3.56.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2022,8,29]],"date-time":"2022-08-29T00:00:00Z","timestamp":1661731200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,8,29]]},"abstract":"<jats:p>The aim of staged compilation is to enable metaprogramming in a way such that we  \nhave guarantees about the well-formedness of code output, and we can also mix  \ntogether object-level and meta-level code in a concise and convenient manner. In  \nthis work, we observe that two-level type theory (2LTT), a system originally  \ndevised for the purpose of developing synthetic homotopy theory, also serves as  \na system for staged compilation with dependent types. 2LTT has numerous good  \nproperties for this use case: it has a concise specification, well-behaved model  \ntheory, and it supports a wide range of language features both at the object and  \nthe meta level. First, we give an overview of 2LTT's features and applications  \nin staging. Then, we present a staging algorithm and prove its correctness. Our  \nalgorithm is \"staging-by-evaluation\", analogously to the technique of  \nnormalization-by-evaluation, in that staging is given by the evaluation of 2LTT  \nsyntax in a semantic domain. The staging algorithm together with its correctness  \nconstitutes a proof of strong conservativity of 2LLT over the object theory. To our  \nknowledge, this is the first description of staged compilation which supports  \nfull dependent types and unrestricted staging for types.<\/jats:p>","DOI":"10.1145\/3547641","type":"journal-article","created":{"date-parts":[[2022,8,31]],"date-time":"2022-08-31T15:39:26Z","timestamp":1661960366000},"page":"540-569","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Staged compilation with two-level type theory"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6375-9781","authenticated-orcid":false,"given":"Andr\u00e1s","family":"Kov\u00e1cs","sequence":"first","affiliation":[{"name":"E\u00f6tv\u00f6s Lor\u00e1nd University, Hungary"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,8,31]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"345","article-title":"Untyped Algorithmic Equality for Martin-L\u00f6f\u2019s Logical Framework with Surjective Pairs","volume":"77","author":"Abel Andreas","year":"2007","unstructured":"Andreas Abel and Thierry Coquand . 2007 . Untyped Algorithmic Equality for Martin-L\u00f6f\u2019s Logical Framework with Surjective Pairs . Fundam. Informaticae , 77 , 4 (2007), 345 \u2013 395 . http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi77-4-05 Andreas Abel and Thierry Coquand. 2007. Untyped Algorithmic Equality for Martin-L\u00f6f\u2019s Logical Framework with Surjective Pairs. Fundam. Informaticae, 77, 4 (2007), 345\u2013395. http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi77-4-05","journal-title":"Fundam. Informaticae"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:4)2011"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_2_1_4_1","unstructured":"Agda developers. 2022. Agda documentation. https:\/\/agda.readthedocs.io\/en\/v2.6.2.1\/ \t\t\t\t  Agda developers. 2022. Agda documentation. https:\/\/agda.readthedocs.io\/en\/v2.6.2.1\/"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:1)2017"},{"key":"e_1_2_1_7_1","unstructured":"Danil Annenkov Paolo Capriotti Nicolai Kraus and Christian Sattler. 2019. Two-Level Type Theory and Applications. ArXiv e-prints may arxiv:1705.03307 \t\t\t\t  Danil Annenkov Paolo Capriotti Nicolai Kraus and Christian Sattler. 2019. Two-Level Type Theory and Applications. ArXiv e-prints may arxiv:1705.03307"},{"key":"e_1_2_1_8_1","unstructured":"Rafa\u00ebl Bocquet Ambrus Kaposi and Christian Sattler. 2021. Relative induction principles for type theories. arXiv preprint arXiv:2102.11649. \t\t\t\t  Rafa\u00ebl Bocquet Ambrus Kaposi and Christian Sattler. 2021. Relative induction principles for type theories. arXiv preprint arXiv:2102.11649."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90135-5"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863587"},{"key":"e_1_2_1_11_1","unstructured":"Paolo Capriotti. 2017. Models of type theory with strict equality. arXiv preprint arXiv:1702.04912. \t\t\t\t  Paolo Capriotti. 2017. Models of type theory with strict equality. arXiv preprint arXiv:1702.04912."},{"key":"e_1_2_1_12_1","volume-title":"CoRR, abs\/1904.00827","author":"Castellan Simon","year":"2019","unstructured":"Simon Castellan , Pierre Clairambault , and Peter Dybjer . 2019. Categories with Families: Unityped , Simply Typed, and Dependently Typed. CoRR, abs\/1904.00827 ( 2019 ), arXiv:1904.00827. arxiv:1904.00827 Simon Castellan, Pierre Clairambault, and Peter Dybjer. 2019. Categories with Families: Unityped, Simply Typed, and Dependently Typed. CoRR, abs\/1904.00827 (2019), arXiv:1904.00827. arxiv:1904.00827"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2020.14"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1932681.1863547"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00021-6"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.01.015"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291199"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000356"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/236114.236119"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.15760\/etd.5531"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165214"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394736"},{"key":"e_1_2_1_25_1","volume-title":"Extensional concepts in intensional type theory","author":"Hofmann Martin","unstructured":"Martin Hofmann . 1995. Extensional concepts in intensional type theory . University of Edinburgh , Department of Computer Science. Martin Hofmann. 1995. Extensional concepts in intensional type theory. University of Edinburgh, Department of Computer Science."},{"key":"e_1_2_1_26_1","volume-title":"Semantics and Logics of Computation","author":"Hofmann Martin","unstructured":"Martin Hofmann . 1997. Syntax and Semantics of Dependent Types . In Semantics and Logics of Computation . Cambridge University Press , 79\u2013130. Martin Hofmann. 1997. Syntax and Semantics of Dependent Types. In Semantics and Logics of Computation. Cambridge University Press, 79\u2013130."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782616"},{"key":"e_1_2_1_28_1","volume-title":"A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types. CoRR, abs\/2206.02831","author":"Hu Jason Z. S.","year":"2022","unstructured":"Jason Z. S. Hu , Brigitte Pientka , and Ulrich Sch\u00f6pp . 2022. A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types. CoRR, abs\/2206.02831 ( 2022 ), https:\/\/doi.org\/10.48550\/arXiv.2206.02831 arXiv:2206.02831. Jason Z. S. Hu, Brigitte Pientka, and Ulrich Sch\u00f6pp. 2022. A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types. CoRR, abs\/2206.02831 (2022), https:\/\/doi.org\/10.48550\/arXiv.2206.02831 arXiv:2206.02831."},{"key":"e_1_2_1_29_1","volume-title":"Cubical Interpretations of Type Theory. Ph. D. Dissertation","author":"Huber Simon","unstructured":"Simon Huber . 2016. Cubical Interpretations of Type Theory. Ph. D. Dissertation . University of Gothenburg. Simon Huber. 2016. Cubical Interpretations of Type Theory. Ph. D. Dissertation. University of Gothenburg."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498700"},{"key":"e_1_2_1_31_1","volume-title":"Partial evaluation and automatic program generation","author":"Jones Neil D.","year":"2024","unstructured":"Neil D. Jones , Carsten K. Gomard , and Peter Sestoft . 1993. Partial evaluation and automatic program generation . Prentice Hall . isbn:978-0-13-0 2024 9-9 Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. 1993. Partial evaluation and automatic program generation. Prentice Hall. isbn:978-0-13-020249-9"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000256"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.25"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_4"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_6"},{"key":"e_1_2_1_37_1","volume-title":"Lights or Magic. CoRR, abs\/2201.00495","author":"Kiselyov Oleg","year":"2022","unstructured":"Oleg Kiselyov and Jeremy Yallop . 2022. let (rec) insertion without Effects , Lights or Magic. CoRR, abs\/2201.00495 ( 2022 ), arXiv:2201.00495. arxiv:2201.00495 Oleg Kiselyov and Jeremy Yallop. 2022. let (rec) insertion without Effects, Lights or Magic. CoRR, abs\/2201.00495 (2022), arXiv:2201.00495. arxiv:2201.00495"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6757373"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2018.22"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2036918.2036920"},{"key":"e_1_2_1_41_1","volume-title":"Categories for the Working Mathematician","author":"Lane Saunders Mac","unstructured":"Saunders Mac Lane . 1998. Categories for the Working Mathematician ( 2 nd ed.). Springer . isbn:0387984038 http:\/\/www.amazon.com\/exec\/obidos\/redirect?tag=citeulike07-20&path=ASIN\/0387984038 Saunders Mac Lane. 1998. Categories for the Working Mathematician (2nd ed.). Springer. isbn:0387984038 http:\/\/www.amazon.com\/exec\/obidos\/redirect?tag=citeulike07-20&path=ASIN\/0387984038","edition":"2"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2016.24"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/636517.636528"},{"key":"e_1_2_1_46_1","volume-title":"First Steps in Synthetic Tait Computability. Ph. D. Dissertation","author":"Sterling Jonathan","unstructured":"Jonathan Sterling . 2021. First Steps in Synthetic Tait Computability. Ph. D. Dissertation . Carnegie Mellon University Pittsburgh , PA. Jonathan Sterling. 2021. First Steps in Synthetic Tait Computability. Ph. D. Dissertation. Carnegie Mellon University Pittsburgh, PA."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS52264.2021.9470719"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"e_1_2_1_49_1","unstructured":"Vladimir Voevodsky. 2013. A simple type system with two identity types. Unpublished note \t\t\t\t  Vladimir Voevodsky. 2013. A simple type system with two identity types. Unpublished note"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294095"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498723"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236795"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547641","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3547641","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:43:29Z","timestamp":1750257809000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3547641"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,29]]},"references-count":52,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2022,8,29]]}},"alternative-id":["10.1145\/3547641"],"URL":"https:\/\/doi.org\/10.1145\/3547641","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,8,29]]},"assertion":[{"value":"2022-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}