{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:44:34Z","timestamp":1770281074519,"version":"3.49.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1823244,1518844"],"award-info":[{"award-number":["1823244,1518844"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100002790","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["GS501100000023"],"award-info":[{"award-number":["GS501100000023"]}],"id":[{"id":"10.13039\/501100002790","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":[[2020,1]]},"abstract":"<jats:p>We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages.<\/jats:p>\n          <jats:p>With it, programmers may rapidly prototype and iterate on the design of new dependently typed features and extensions.<\/jats:p>\n          <jats:p>Or they may create entirely new DSLs whose dependent type ``power'' is tailored to a specific domain.<\/jats:p>\n          <jats:p>Our framework's support of language-oriented programming also makes it suitable for experimenting with systems of interacting components, e.g., a proof assistant and its companion DSLs.<\/jats:p>\n          <jats:p>This paper explains the implementation details of Turnstile+, as well as how it may be used to create a wide-variety of dependently typed languages, from a lightweight one with indexed types, to a full spectrum proof assistant, complete with a tactic system and extensions for features like sized types and SMT interaction.<\/jats:p>","DOI":"10.1145\/3371071","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Dependent type systems as macros"],"prefix":"10.1145","volume":"4","author":[{"given":"Stephen","family":"Chang","sequence":"first","affiliation":[{"name":"Northeastern University, USA \/ PLT Group, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Ballantyne","sequence":"additional","affiliation":[{"name":"Northeastern University, USA \/ PLT Group, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Milo","family":"Turner","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William J.","family":"Bowman","sequence":"additional","affiliation":[{"name":"University of British Columbia, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"2017. RFC: The pi type trilogy. https:\/\/github.com\/rust-lang\/rfcs\/issues\/1930  2017. RFC: The pi type trilogy. https:\/\/github.com\/rust-lang\/rfcs\/issues\/1930"},{"key":"e_1_2_2_2_1","volume-title":"PAR (EPTCS)","author":"Abel Andreas"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.77.1"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_5"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660216"},{"key":"e_1_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Abhishek Anand Simon Boulier Cyril Cohen Matthieu Sozeau and Nicolas Tabareau. 2018. Towards Certified MetaProgramming with Typed Template-Coq. (2018). www.irif.fr\/~sozeau\/research\/publications\/drafts\/Towards_Certified_ Meta-Programming_with_Typed_Template-Coq.pdf  Abhishek Anand Simon Boulier Cyril Cohen Matthieu Sozeau and Nicolas Tabareau. 2018. Towards Certified MetaProgramming with Typed Template-Coq. (2018). www.irif.fr\/~sozeau\/research\/publications\/drafts\/Towards_Certified_ Meta-Programming_with_Typed_Template-Coq.pdf","DOI":"10.1007\/978-3-319-94821-8_2"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110274"},{"key":"e_1_2_2_8_1","unstructured":"Lennart Augustsson. 2007. Simpler Easier! http:\/\/augustss.blogspot.ru\/2007\/10\/simpler-easier-in-recent-paper-simply.html  Lennart Augustsson. 2007. Simpler Easier! http:\/\/augustss.blogspot.ru\/2007\/10\/simpler-easier-in-recent-paper-simply.html"},{"key":"e_1_2_2_9_1","unstructured":"Andrej Bauer. 2012. How to Implement Dependent Type Theory. http:\/\/math.andrej.com\/2012\/11\/08\/how-to-implementdependent-type-theory-i\/  Andrej Bauer. 2012. How to Implement Dependent Type Theory. http:\/\/math.andrej.com\/2012\/11\/08\/how-to-implementdependent-type-theory-i\/"},{"key":"e_1_2_2_10_1","first-page":"101","article-title":"Hammering towards QED","volume":"9","author":"Blanchette Jasmin C.","year":"2016","journal-title":"J. Formaliz. Reason."},{"key":"e_1_2_2_11_1","volume-title":"Dependently Typed MetaProgramming. In 7th Symposium on Trends in Functional Programming.","author":"Brady Edwin","year":"2006"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009886"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951932"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628139"},{"key":"e_1_2_2_16_1","volume-title":"Proceedings of the Workshop on Types for Proofs and Programs. 71\u201383","author":"Coquand Thierry","year":"1992"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11821069_1"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90066-B"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44404-1_7"},{"key":"e_1_2_2_21_1","volume-title":"Typed Syntactic Meta-programming. In of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP","author":"Devriese Dominique","year":"2013"},{"key":"e_1_2_2_22_1","volume-title":"Inductive families. Formal Aspects of Computing 6, 4 (01","author":"Dybjer Peter","year":"1994"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01806308"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_2_2_25_1","volume-title":"Matthew Flatt, Shriram Krishnamurthi, Eli Barzilay, Jay McCarthy, and Sam Tobin-Hochstadt.","author":"Felleisen Matthias","year":"2015"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3127323"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581486"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837620"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000093"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_3"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_27"},{"key":"e_1_2_2_32_1","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier Georges","year":"2010","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034798"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3240719.3241791"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1883634.1883637"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_21"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"e_1_2_2_42_1","volume-title":"Smith","author":"Nordstr\u00f6m Bengt","year":"1990"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"e_1_2_2_45_1","volume-title":"Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u02c7 at\u02c7 alin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey.","author":"Pierce Benjamin C.","year":"2018"},{"key":"e_1_2_2_46_1","volume-title":"Proceedings of the 25th ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages. 252\u2013265","author":"Benjamin"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784755"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291155"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863591"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_2_51_1","unstructured":"Stephanie Weirich. 2014. Pi Forall: notes from OPLSS. https:\/\/github.com\/sweirich\/pi-forall  Stephanie Weirich. 2014. Pi Forall: notes from OPLSS. https:\/\/github.com\/sweirich\/pi-forall"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806006216"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103786.2103795"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500579"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134043"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371071","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371071","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371071","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:42Z","timestamp":1750273542000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371071"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":53,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371071"],"URL":"https:\/\/doi.org\/10.1145\/3371071","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}