{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T01:12:59Z","timestamp":1740100379867,"version":"3.37.3"},"publisher-location":"New York, NY, USA","reference-count":34,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,10,17]]},"DOI":"10.1145\/3486609.3487201","type":"proceedings-article","created":{"date-parts":[[2021,11,22]],"date-time":"2021-11-22T22:14:41Z","timestamp":1637619281000},"page":"83-95","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Extracting the power of dependent types"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3292-2985","authenticated-orcid":false,"given":"Artjoms","family":"\u0160inkarovs","sequence":"first","affiliation":[{"name":"Heriot-Watt University, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3862-4073","authenticated-orcid":false,"given":"Jesper","family":"Cockx","sequence":"additional","affiliation":[{"name":"TU Delft, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2021,11,22]]},"reference":[{"volume-title":"PostScript Language Reference","author":"Incorporated Adobe Systems","key":"e_1_3_2_1_1_1","unstructured":"Adobe Systems Incorporated . 1999. PostScript Language Reference Third Edition. Adobe Systems Incorporated. 1999. PostScript Language Reference Third Edition."},{"key":"e_1_3_2_1_2_1","unstructured":"Agda Development Team. 2021. Agda 2.6.2 documentation. https:\/\/agda.readthedocs.io\/en\/v2.6.2\/ Accessed [2021\/07\/10]. Agda Development Team. 2021. Agda 2.6.2 documentation. https:\/\/agda.readthedocs.io\/en\/v2.6.2\/ Accessed [2021\/07\/10]."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236785"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/647849.737066"},{"volume-title":"Towards Certified Meta-Programming with Typed Template-Coq","author":"Anand Abhishek","key":"e_1_3_2_1_5_1","unstructured":"Abhishek Anand , Simon Boulier , Cyril Cohen , Matthieu Sozeau , and Nicolas Tabareau . 2018. Towards Certified Meta-Programming with Typed Template-Coq . In Interactive Theorem Proving, Jeremy Avigad and Assia Mahboubi (Eds.). Springer International Publishing , Cham . 20\u201339. isbn:978-3-319-94821-8 Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. 2018. Towards Certified Meta-Programming with Typed Template-Coq. In Interactive Theorem Proving, Jeremy Avigad and Assia Mahboubi (Eds.). Springer International Publishing, Cham. 20\u201339. isbn:978-3-319-94821-8"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373829"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"volume-title":"Partially Evaluated","author":"Carette Jacques","key":"e_1_3_2_1_8_1","unstructured":"Jacques Carette , Oleg Kiselyov , and Chung-chieh Shan. 2007. Finally Tagless , Partially Evaluated . In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 222\u2013238. isbn:978-3-540-76637-7 Jacques Carette, Oleg Kiselyov, and Chung-chieh Shan. 2007. Finally Tagless, Partially Evaluated. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 222\u2013238. isbn:978-3-540-76637-7"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371071"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951932"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2019.2"},{"key":"e_1_3_2_1_13_1","unstructured":"The Coq Development Team. 2021. The Coq proof assistant reference manual. https:\/\/coq.github.io\/doc\/v8.13\/refman\/ Version 8.13.2. The Coq Development Team. 2021. The Coq proof assistant reference manual. https:\/\/coq.github.io\/doc\/v8.13\/refman\/ Version 8.13.2."},{"volume-title":"Types for Proofs and Programs","author":"Danielsson Nils Anders","key":"e_1_3_2_1_14_1","unstructured":"Nils Anders Danielsson . 2007. A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family . In Types for Proofs and Programs , Thorsten Altenkirch and Conor McBride (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 93\u2013109. isbn:978-3-540-74464-1 Nils Anders Danielsson. 2007. A Formalisation of a Dependently Typed Language as an Inductive-Recursive Family. In Types for Proofs and Programs, Thorsten Altenkirch and Conor McBride (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 93\u2013109. isbn:978-3-540-74464-1"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_3_2_1_16_1","volume-title":"Reference: Racket","author":"Flatt Matthew","year":"2010","unstructured":"Matthew Flatt and PLT. 2010 . Reference: Racket . PLT Design Inc .. https:\/\/racket-lang.org\/tr1\/ Matthew Flatt and PLT. 2010. Reference: Racket. PLT Design Inc.. https:\/\/racket-lang.org\/tr1\/"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005757"},{"volume-title":"Reflection for the Masses","author":"Herzeel Charlotte","key":"e_1_3_2_1_18_1","unstructured":"Charlotte Herzeel , Pascal Costanza , and Theo D\u2019Hondt . 2008. Reflection for the Masses . In Self-Sustaining Systems, Robert Hirschfeld and Kim Rose (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 87\u2013122. isbn:978-3-540-89275-5 Charlotte Herzeel, Pascal Costanza, and Theo D\u2019Hondt. 2008. Reflection for the Masses. In Self-Sustaining Systems, Robert Hirschfeld and Kim Rose (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 87\u2013122. isbn:978-3-540-89275-5"},{"volume-title":"The Design and Implementation of MetaOCaml","author":"Kiselyov Oleg","key":"e_1_3_2_1_19_1","unstructured":"Oleg Kiselyov . 2014. The Design and Implementation of MetaOCaml . In Functional and Logic Programming, Michael Codish and Eijiro Sumii (Eds.). Springer International Publishing , Cham . 86\u2013102. isbn:978-3-319-07151-0 Oleg Kiselyov. 2014. The Design and Implementation of MetaOCaml. In Functional and Logic Programming, Michael Codish and Eijiro Sumii (Eds.). Springer International Publishing, Cham. 86\u2013102. isbn:978-3-319-07151-0"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"volume-title":"Types for Proofs and Programs","author":"Letouzey Pierre","key":"e_1_3_2_1_22_1","unstructured":"Pierre Letouzey . 2003. A New Extraction for Coq . In Types for Proofs and Programs , Herman Geuvers and Freek Wiedijk (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 200\u2013219. isbn:978-3-540-39185-2 Pierre Letouzey. 2003. A New Extraction for Coq. In Types for Proofs and Programs, Herman Geuvers and Freek Wiedijk (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 200\u2013219. isbn:978-3-540-39185-2"},{"volume-title":"Logic and Theory of Algorithms, Arnold Beckmann, Costas Dimitracopoulos, and Benedikt L\u00f6we (Eds.)","author":"Letouzey Pierre","key":"e_1_3_2_1_23_1","unstructured":"Pierre Letouzey . 2008. Extraction in Coq: An Overview . In Logic and Theory of Algorithms, Arnold Beckmann, Costas Dimitracopoulos, and Benedikt L\u00f6we (Eds.) . Springer Berlin Heidelberg, Berlin , Heidelberg . 359\u2013369. isbn:978-3-540-69407-6 Pierre Letouzey. 2008. Extraction in Coq: An Overview. In Logic and Theory of Algorithms, Arnold Beckmann, Costas Dimitracopoulos, and Benedikt L\u00f6we (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 359\u2013369. isbn:978-3-540-69407-6"},{"key":"e_1_3_2_1_24_1","volume-title":"Twenty-five years of constructive type theory (Venice","author":"Martin-L\u00f6f Per","year":"1995","unstructured":"Per Martin-L\u00f6f . 1998. An intuitionistic theory of types . In Twenty-five years of constructive type theory (Venice , 1995 ), Giovanni Sambin and Jan M. Smith (Eds.) (Oxford Logic Guides , Vol. 36). Oxford University Press, 127\u2013 172 . Per Martin-L\u00f6f. 1998. An intuitionistic theory of types. In Twenty-five years of constructive type theory (Venice, 1995), Giovanni Sambin and Jan M. Smith (Eds.) (Oxford Logic Guides, Vol. 36). Oxford University Press, 127\u2013172."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863495.1863497"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581499"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581691"},{"key":"e_1_3_2_1_29_1","volume-title":"Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection. CoRR, abs\/2105.10819","author":"Sinkarovs Artjoms","year":"2021","unstructured":"Artjoms Sinkarovs and Jesper Cockx . 2021. Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection. CoRR, abs\/2105.10819 ( 2021 ), arxiv:2105.10819. arxiv:2105.10819 Artjoms Sinkarovs and Jesper Cockx. 2021. Choosing is Losing: How to combine the benefits of shallow and deep embeddings through reflection. CoRR, abs\/2105.10819 (2021), arxiv:2105.10819. arxiv:2105.10819"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/800017.800513"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371076"},{"volume-title":"Trends in Functional Programming, Hans-Wolfgang Loidl and Ricardo Pe\u00f1a (Eds.)","author":"Svenningsson Josef","key":"e_1_3_2_1_32_1","unstructured":"Josef Svenningsson and Emil Axelsson . 2013. Combining Deep and Shallow Embedding for EDSL . In Trends in Functional Programming, Hans-Wolfgang Loidl and Ricardo Pe\u00f1a (Eds.) . Springer Berlin Heidelberg , Berlin, Heidelberg . 21\u201336. isbn:978-3-642-40447-4 Josef Svenningsson and Emil Axelsson. 2013. Combining Deep and Shallow Embedding for EDSL. In Trends in Functional Programming, Hans-Wolfgang Loidl and Ricardo Pe\u00f1a (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 21\u201336. isbn:978-3-642-40447-4"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/258994.259019"},{"volume-title":"Implementation and Application of Functional Languages","author":"van der Walt Paul","key":"e_1_3_2_1_34_1","unstructured":"Paul van der Walt and Wouter Swierstra . 2013. Engineering Proof by Reflection in Agda . In Implementation and Application of Functional Languages , Ralf Hinze (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 157\u2013173. isbn:978-3-642-41582-1 Paul van der Walt and Wouter Swierstra. 2013. Engineering Proof by Reflection in Agda. In Implementation and Application of Functional Languages, Ralf Hinze (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 157\u2013173. isbn:978-3-642-41582-1"}],"event":{"name":"GPCE '21: Concepts and Experiences","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Chicago IL USA","acronym":"GPCE '21"},"container-title":["Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3486609.3487201","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T09:31:54Z","timestamp":1673083914000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3486609.3487201"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,17]]},"references-count":34,"alternative-id":["10.1145\/3486609.3487201","10.1145\/3486609"],"URL":"https:\/\/doi.org\/10.1145\/3486609.3487201","relation":{},"subject":[],"published":{"date-parts":[[2021,10,17]]},"assertion":[{"value":"2021-11-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}