{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:03:28Z","timestamp":1767927808937,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,8,18]],"date-time":"2019-08-18T00:00:00Z","timestamp":1566086400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/M016951\/1"],"award-info":[{"award-number":["EP\/M016951\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,8,18]]},"DOI":"10.1145\/3331554.3342604","type":"proceedings-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:51:45Z","timestamp":1564433505000},"page":"14-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Generic level polymorphic n-ary functions"],"prefix":"10.1145","author":[{"given":"Guillaume","family":"Allais","sequence":"first","affiliation":[{"name":"University of Strathclyde, UK"}]}],"member":"320","published-online":{"date-parts":[[2019,8,18]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings (Lecture Notes in Computer Science), C.-H. Luke Ong (Ed.)","volume":"6690","author":"Abel Andreas","year":"2011","unstructured":"Andreas Abel and Brigitte Pientka . 2011 . Higher-Order Dynamic Pattern Unification for Dependent Types and Records. In Typed Lambda Calculi and Applications - 10th International Conference , TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings (Lecture Notes in Computer Science), C.-H. Luke Ong (Ed.) , Vol. 6690 . Springer, 10\u201326. Andreas Abel and Brigitte Pientka. 2011. Higher-Order Dynamic Pattern Unification for Dependent Types and Records. In Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings (Lecture Notes in Computer Science), C.-H. Luke Ong (Ed.), Vol. 6690. Springer, 10\u201326."},{"key":"e_1_3_2_1_2_1","volume-title":"ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (Lecture Notes in Computer Science), Jeremy Avigad and Assia Mahboubi (Eds.)","volume":"10895","author":"Anand Abhishek","year":"2018","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 - 9th International Conference , ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (Lecture Notes in Computer Science), Jeremy Avigad and Assia Mahboubi (Eds.) , Vol. 10895 . Springer, 20\u201339. Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. 2018. Towards Certified Meta-Programming with Typed Template-Coq. In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings (Lecture Notes in Computer Science), Jeremy Avigad and Assia Mahboubi (Eds.), Vol. 10895. Springer, 20\u201339."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-012-9087-2"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289451"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000056"},{"key":"e_1_3_2_1_6_1","volume-title":"Implementation and Application of Functional Languages -20th International Symposium, IFL","author":"Danielsson Nils Anders","year":"2008","unstructured":"Nils Anders Danielsson and Ulf Norell . 2008. Parsing Mixfix Operators . In Implementation and Application of Functional Languages -20th International Symposium, IFL 2008 , Hatfield, UK , September 10-12, 2008. Revised Selected Papers (Lecture Notes in Computer Science), Sven-Bodo Scholz and Olaf Chitil (Eds.), Vol. 5836 . Springer , 80\u201399. Nils Anders Danielsson and Ulf Norell. 2008. Parsing Mixfix Operators. In Implementation and Application of Functional Languages -20th International Symposium, IFL 2008, Hatfield, UK, September 10-12, 2008. Revised Selected Papers (Lecture Notes in Computer Science), Sven-Bodo Scholz and Olaf Chitil (Eds.), Vol. 5836. Springer, 80\u201399."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003104"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003658"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325709"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/242224.242477"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004355"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_3_2_1_16_1","unstructured":"Matthieu Sozeau Abhishek Anand Simon Boulier Cyril Cohen Yannick Forster Fabian Kunze Gregory Malecha Nicolas Tabareau and Th\u00e9o Winterhalter. 2018. The MetaCoq Project. (2018). Unpublished draft extended version of the ITP18 paper.  Matthieu Sozeau Abhishek Anand Simon Boulier Cyril Cohen Yannick Forster Fabian Kunze Gregory Malecha Nicolas Tabareau and Th\u00e9o Winterhalter. 2018. The MetaCoq Project. (2018). Unpublished draft extended version of the ITP18 paper."},{"key":"e_1_3_2_1_17_1","first-page":"751","article-title":"Total Functional Programming","volume":"10","author":"Turner D. A.","year":"2004","unstructured":"D. A. Turner . 2004 . Total Functional Programming . J. UCS 10 , 7 (2004), 751 \u2013 768 . D. A. Turner. 2004. Total Functional Programming. J. UCS 10, 7 (2004), 751\u2013768.","journal-title":"J. UCS"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411318.1411326"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707790.1707799"}],"event":{"name":"ICFP '19: ACM SIGPLAN International Conference on Functional Programming","location":"Berlin Germany","acronym":"ICFP '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 4th ACM SIGPLAN International Workshop on Type-Driven Development"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331554.3342604","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3331554.3342604","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:13:39Z","timestamp":1750202019000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3331554.3342604"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,18]]},"references-count":19,"alternative-id":["10.1145\/3331554.3342604","10.1145\/3331554"],"URL":"https:\/\/doi.org\/10.1145\/3331554.3342604","relation":{},"subject":[],"published":{"date-parts":[[2019,8,18]]},"assertion":[{"value":"2019-08-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}