{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:21Z","timestamp":1775790741282,"version":"3.50.1"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319948201","type":"print"},{"value":"9783319948218","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94821-8_2","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T13:25:55Z","timestamp":1530624355000},"page":"20-39","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Towards Certified Meta-Programming with Typed Template-Coq"],"prefix":"10.1007","author":[{"given":"Abhishek","family":"Anand","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Simon","family":"Boulier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cyril","family":"Cohen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matthieu","family":"Sozeau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicolas","family":"Tabareau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"issue":"POPL","key":"2_CR1","first-page":"23:1","volume":"2","author":"A Abel","year":"2018","unstructured":"Abel, A., \u00d6hman, J., Vezzosi, A.: Decidability of conversion for type theory in type theory. PACMPL 2(POPL), 23:1\u201323:29 (2018). \n                    http:\/\/doi.acm.org\/10.1145\/3158111","journal-title":"PACMPL"},{"key":"2_CR2","unstructured":"Altenkirch, T., Kaposi, A.: Type theory in type theory using quotient inductive types. In: POPL 2016, pp. 18\u201329. ACM, New York (2016). \n                    http:\/\/doi.acm.org\/10.1145\/2837614.2837638"},{"key":"2_CR3","unstructured":"Anand, A., Morrisett, G.: Revisiting parametricity: inductives and uniformity of propositions. In: CoqPL 2018, Los Angeles, CA, USA (2018)"},{"key":"2_CR4","unstructured":"Anand, A., Appel, A., Morrisett, G., Paraskevopoulou, Z., Pollack, R.,Belanger, O.S., Sozeau, M., Weaver, M.: CertiCoq: a verified compiler for Coq. In: CoqPL, Paris, France (2017). \n                    http:\/\/conf.researchr.org\/event\/CoqPL-2017\/main-certicoq-a-verified-compiler-for-coq"},{"key":"2_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-14052-5_8","volume-title":"Interactive Theorem Proving","author":"M Armand","year":"2010","unstructured":"Armand, M., Gr\u00e9goire, B., Spiwack, A., Th\u00e9ry, L.: Extending Coq with imperative features and its application to SAT verification. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 83\u201398. Springer, Heidelberg (2010). \n                    https:\/\/doi.org\/10.1007\/978-3-642-14052-5_8"},{"key":"2_CR6","unstructured":"Barras, B.: Auto-validation d\u2019un syst\u00e8me de preuves avec familles inductives. Th\u00e8se de doctorat, Universit\u00e9 Paris 7, November 1999"},{"issue":"2","key":"2_CR7","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1017\/S0956796812000056","volume":"22","author":"JP Bernardy","year":"2012","unstructured":"Bernardy, J.P., Jansson, P., Paterson, R.: Proofs for free: parametricity for dependent types. J. Funct. Program. 22(2), 107\u2013152 (2012)","journal-title":"J. Funct. Program."},{"key":"2_CR8","doi-asserted-by":"crossref","unstructured":"Boulier, S., P\u00e9drot, P.M., Tabareau, N.: The next 700 syntactical models of type theory. In: CPP 2017, pp. 182\u2013194. ACM, Paris (2017)","DOI":"10.1145\/3018610.3018620"},{"key":"2_CR9","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.entcs.2008.12.114","volume":"228","author":"J Chapman","year":"2009","unstructured":"Chapman, J.: Type theory should eat itself. Electron. Notes Theor. Comput. Sci. 228, 21\u201336 (2009). Proceedings of LFMTP 2008. \n                    http:\/\/www.sciencedirect.com\/science\/article\/pii\/S157106610800577X","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"2_CR10","volume-title":"Certified Programming with Dependent Types","author":"A Chlipala","year":"2011","unstructured":"Chlipala, A.: Certified Programming with Dependent Types, vol. 20. MIT Press, Cambridge (2011)"},{"key":"2_CR11","unstructured":"Devriese, D., Piessens, F.: Typed syntactic meta-programming. In: ICFP 2013, vol. 48, pp. 73\u201386. ACM (2013). \n                    http:\/\/doi.acm.org\/10.1145\/2500365.2500575"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Ebner, G., Ullrich, S., Roesch, J., Avigad, J., de Moura, L.: A metaprogramming framework for formal verification, pp. 34:1\u201334:29, September 2017","DOI":"10.1145\/3110278"},{"key":"2_CR13","unstructured":"Forster, Y., Kunze, F.: Verified extraction from Coq to a lambda-calculus. In: Coq Workshop 2016 (2016). \n                    https:\/\/www.ps.uni-saarland.de\/forster\/coq-workshop-16\/abstract-coq-ws-16.pdf"},{"key":"2_CR14","unstructured":"Jaber, G., Lewertowski, G., P\u00e9drot, P.M., Sozeau, M., Tabareau, N.: The definitional side of the forcing. In: LICS 2016, New York, NY, USA, pp. 367\u2013376 (2016). \n                    http:\/\/doi.acm.org\/10.1145\/2933575.2935320"},{"key":"2_CR15","unstructured":"Keller, C., Lasson, M.: Parametricity in an impredicative sort. CoRR abs\/1209.6336 (2012). \n                    http:\/\/arxiv.org\/abs\/1209.6336"},{"key":"2_CR16","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1016\/j.entcs.2014.10.013","volume":"308","author":"M Lasson","year":"2014","unstructured":"Lasson, M.: Canonicity of weak \n                    \n                      \n                    \n                    $$\\omega $$\n                  -groupoid laws using parametricity theory. Electron. Notes Theor. Comput. Sci. 308, 229\u2013244 (2014)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"532","DOI":"10.1007\/978-3-662-49498-1_21","volume-title":"Programming Languages and Systems","author":"G Malecha","year":"2016","unstructured":"Malecha, G., Bengtson, J.: Extensible and efficient automation through reflective tactics. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 532\u2013559. Springer, Heidelberg (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-662-49498-1_21"},{"key":"2_CR18","unstructured":"Malecha, G.M.: Extensible proof engineering in intensional type theory. Ph.D. thesis, Harvard University (2014)"},{"key":"2_CR19","unstructured":"Mullen, E., Pernsteiner, S., Wilcox, J.R., Tatlock, Z., Grossman, D.: \u0152uf: minimizing the Coq extraction TCB. In: Proceedings of CPP 2018, pp. 172\u2013185 (2018). \n                    http:\/\/doi.acm.org\/10.1145\/3167089"},{"key":"2_CR20","doi-asserted-by":"publisher","unstructured":"P\u00e9drot, P., Tabareau, N.: An effectful way to eliminate addiction to dependence. In: LICS 2017, Reykjavik, Iceland, pp. 1\u201312 (2017). \n                    https:\/\/doi.org\/10.1109\/LICS.2017.8005113","DOI":"10.1109\/LICS.2017.8005113"},{"key":"2_CR21","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513\u2013523 (1983)"},{"issue":"12","key":"2_CR22","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1145\/636517.636528","volume":"37","author":"T Sheard","year":"2002","unstructured":"Sheard, T., Jones, S.P.: Template meta-programming for Haskell. SIGPLAN Not. 37(12), 60\u201375 (2002). \n                    http:\/\/doi.acm.org\/10.1145\/636517.636528","journal-title":"SIGPLAN Not."},{"key":"2_CR23","unstructured":"Sozeau, M.: Programming finger trees in Coq. In: ICFP 2007, pp. 13\u201324. ACM, New York (2007). \n                    http:\/\/doi.acm.org\/10.1145\/1291151.1291156"},{"key":"2_CR24","unstructured":"Taha, W., Sheard, T.: Multi-stage programming with explicit annotations. In: PEPM 1997, pp. 203\u2013217. ACM, New York (1997). \n                    http:\/\/doi.acm.org\/10.1145\/258993.259019"},{"key":"2_CR25","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Theorems for free! In: Functional Programming Languages and Computer Architecture, pp. 347\u2013359. ACM Press (1989)","DOI":"10.1145\/99370.99404"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-642-41582-1_10","volume-title":"Implementation and Application of Functional Languages","author":"P Walt van der","year":"2013","unstructured":"van der Walt, P., Swierstra, W.: Engineering proof by reflection in Agda. In: Hinze, R. (ed.) IFL 2012. LNCS, vol. 8241, pp. 157\u2013173. Springer, Heidelberg (2013). \n                    https:\/\/doi.org\/10.1007\/978-3-642-41582-1_10"},{"key":"2_CR27","doi-asserted-by":"publisher","unstructured":"Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: a monad for typed tactic programming in Coq. J. Funct. Program. 25 (2015). \n                    https:\/\/doi.org\/10.1017\/S0956796815000118","DOI":"10.1017\/S0956796815000118"},{"key":"2_CR28","doi-asserted-by":"publisher","first-page":"e10","DOI":"10.1017\/S0956796817000028","volume":"27","author":"B Ziliani","year":"2017","unstructured":"Ziliani, B., Sozeau, M.: A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. J. Funct. Program. 27, e10 (2017). \n                    http:\/\/www.irif.univ-paris-diderot.fr\/sozeau\/research\/publications\/drafts\/unification-jfp.pdf","journal-title":"J. Funct. Program."}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94821-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T04:10:26Z","timestamp":1558325426000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94821-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319948201","9783319948218"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94821-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"4 July 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ITP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Interactive Theorem Proving","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"itp2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/itp2018.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}