{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:27:15Z","timestamp":1750220835820,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":24,"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"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,8,18]]},"DOI":"10.1145\/3331554.3342607","type":"proceedings-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:51:45Z","timestamp":1564433505000},"page":"52-63","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Inductive types deconstructed: the calculus of united constructions"],"prefix":"10.1145","author":[{"given":"Stefan","family":"Monnier","sequence":"first","affiliation":[{"name":"Universit\u00e9 de Montr\u00e9al, Canada"}]}],"member":"320","published-online":{"date-parts":[[2019,8,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_5"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800020025"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792829"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159836"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535883"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951928"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"e_1_3_2_1_9_1","volume-title":"Pattern Matching with Dependent Types. In Workshop on Types for Proofs and Programs. 66\u201379","author":"Coquand Thierry","year":"1992","unstructured":"Thierry Coquand . 1992 . Pattern Matching with Dependent Types. In Workshop on Types for Proofs and Programs. 66\u201379 . Thierry Coquand. 1992. Pattern Matching with Dependent Types. In Workshop on Types for Proofs and Programs. 66\u201379."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167087"},{"key":"e_1_3_2_1_12_1","unstructured":"G\u00e9rard P. Huet Christine Paulin-Mohring etal 2000. The Coq Proof Assistant Reference Manual. Part of the Coq system version 6.3.1.  G\u00e9rard P. Huet Christine Paulin-Mohring et al. 2000. The Coq Proof Assistant Reference Manual. Part of the Coq system version 6.3.1."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143205"},{"key":"e_1_3_2_1_14_1","volume-title":"The Effectiveness of Type-Based Unboxing. In International Workshop on Types in Compilation. BCCS-97-03","author":"Leroy Xavier","year":"1997","unstructured":"Xavier Leroy . 1997 . The Effectiveness of Type-Based Unboxing. In International Workshop on Types in Compilation. BCCS-97-03 . Xavier Leroy. 1997. The Effectiveness of Type-Based Unboxing. In International Workshop on Types in Compilation. BCCS-97-03."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77390"},{"key":"e_1_3_2_1_16_1","volume-title":"MacQueen","author":"Milner Robin","year":"1997","unstructured":"Robin Milner , Mads Tofte , Robert Harper , and David B . MacQueen . 1997 . The Definition of Standard ML Revised. MIT Press , Cambridge, Massachusetts. Robin Milner, Mads Tofte, Robert Harper, and David B. MacQueen. 1997. The Definition of Standard ML Revised. MIT Press, Cambridge, Massachusetts."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1754621.1754650"},{"key":"e_1_3_2_1_18_1","volume-title":"Erasure and Polymorphism in Pure Type Systems. In Conference on Foundations of Software Science and Computation Structures (Lecture Notes in Computer Science)","volume":"4962","author":"Mishra-Linger Nathan","year":"2008","unstructured":"Nathan Mishra-Linger and Tim Sheard . 2008 . Erasure and Polymorphism in Pure Type Systems. In Conference on Foundations of Software Science and Computation Structures (Lecture Notes in Computer Science) , Vol. 4962 . Budapest, Hungary, 350\u2013364. Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. In Conference on Foundations of Software Science and Computation Structures (Lecture Notes in Computer Science), Vol. 4962. Budapest, Hungary, 350\u2013364."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292597.1292604"},{"key":"e_1_3_2_1_20_1","volume-title":"Typer: ML boosted with type theory and Scheme. In Journ\u00e9es Francophones des Langages Applicatifs. 193\u2013208.","author":"Monnier Stefan","year":"2019","unstructured":"Stefan Monnier . 2019 . Typer: ML boosted with type theory and Scheme. In Journ\u00e9es Francophones des Langages Applicatifs. 193\u2013208. Stefan Monnier. 2019. Typer: ML boosted with type theory and Scheme. In Journ\u00e9es Francophones des Langages Applicatifs. 193\u2013208."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263715"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671440"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/258948.258958"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190315.1190324"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"}],"event":{"name":"ICFP '19: ACM SIGPLAN International Conference on Functional Programming","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Berlin Germany","acronym":"ICFP '19"},"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.3342607","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3331554.3342607","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.3342607"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,8,18]]},"references-count":24,"alternative-id":["10.1145\/3331554.3342607","10.1145\/3331554"],"URL":"https:\/\/doi.org\/10.1145\/3331554.3342607","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"}}]}}