{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T14:08:26Z","timestamp":1762006106104,"version":"build-2065373602"},"publisher-location":"New York, NY, USA","reference-count":24,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,9,27]],"date-time":"2018-09-27T00:00:00Z","timestamp":1538006400000},"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":[[2018,9,27]]},"DOI":"10.1145\/3240719.3241787","type":"proceedings-article","created":{"date-parts":[[2018,9,18]],"date-time":"2018-09-18T12:11:39Z","timestamp":1537272699000},"page":"78-90","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["From algebra to abstract machine: a verified generic construction"],"prefix":"10.1145","author":[{"given":"Carlos","family":"Tom\u00e9 Corti\u00f1as","sequence":"first","affiliation":[{"name":"Utrecht University, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wouter","family":"Swierstra","sequence":"additional","affiliation":[{"name":"Utrecht University, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,9,27]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_1_1","DOI":"10.1016\/j.tcs.2005.06.002"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1145\/888251.888254"},{"doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch Neil Ghani Peter Hancock Conor McBride and Peter Morris. 2015. Indexed containers. Journal of Functional Programming 25 (2015).  Thorsten Altenkirch Neil Ghani Peter Hancock Conor McBride and Peter Morris. 2015. Indexed containers. Journal of Functional Programming 25 (2015).","key":"e_1_3_2_1_3_1","DOI":"10.1017\/S095679681500009X"},{"volume-title":"Generic Programming","author":"Altenkirch Thorsten","key":"e_1_3_2_1_4_1"},{"volume-title":"Spring School on DatatypeGeneric Programming","author":"Altenkirch Thorsten","key":"e_1_3_2_1_5_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.5555\/648084.747162"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1017\/S0960129505004822"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1145\/1863543.1863547"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.1145\/2364527.2364546"},{"doi-asserted-by":"crossref","unstructured":"Olivier Danvy. 2009. From Reduction-Based to Reduction-Free Normalization. Springer Berlin Heidelberg Berlin Heidelberg 66\u2013164.   Olivier Danvy. 2009. From Reduction-Based to Reduction-Free Normalization. Springer Berlin Heidelberg Berlin Heidelberg 66\u2013164.","key":"e_1_3_2_1_10_1","DOI":"10.1007\/978-3-642-04652-0_3"},{"doi-asserted-by":"crossref","unstructured":"Peter Dybjer. 1994. Inductive families. Formal Aspects of Computing 6 4 (01 Jul 1994) 440\u2013465.  Peter Dybjer. 1994. Inductive families. Formal Aspects of Computing 6 4 (01 Jul 1994) 440\u2013465.","key":"e_1_3_2_1_11_1","DOI":"10.1007\/BF01211308"},{"doi-asserted-by":"crossref","unstructured":"Peter Dybjer and Anton Setzer. 1999. A Finite Axiomatization of InductiveRecursive Definitions. In Typed Lambda Calculi and Applications JeanYves Girard (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 129\u2013 146.   Peter Dybjer and Anton Setzer. 1999. A Finite Axiomatization of InductiveRecursive Definitions. In Typed Lambda Calculi and Applications JeanYves Girard (Ed.). Springer Berlin Heidelberg Berlin Heidelberg 129\u2013 146.","key":"e_1_3_2_1_12_1","DOI":"10.1007\/3-540-48959-2_11"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_13_1","DOI":"10.1017\/S0956796897002864"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1093\/comjnl\/6.4.308"},{"unstructured":"Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Vol. 9. Bibliopolis Napoli.  Per Martin-L\u00f6f. 1984. Intuitionistic type theory. Vol. 9. Bibliopolis Napoli.","key":"e_1_3_2_1_15_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_16_1","DOI":"10.1145\/1328438.1328474"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_17_1","DOI":"10.1007\/11617990_16"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_18_1","DOI":"10.1007\/978-3-642-03359-9_26"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_19_1","DOI":"10.1145\/1411318.1411321"},{"unstructured":"Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Chalmers University of Technology.  Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Chalmers University of Technology.","key":"e_1_3_2_1_20_1"},{"volume-title":"International School on Advanced Functional Programming","author":"Norell Ulf","key":"e_1_3_2_1_21_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_22_1","DOI":"10.1145\/1411204.1411213"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.4204\/EPTCS.76.10"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1145\/1596550.1596585"}],"event":{"sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"acronym":"ICFP '18","name":"ICFP '18: 23nd ACM SIGPLAN International Conference on Functional Programming","location":"St. Louis MO USA"},"container-title":["Proceedings of the 3rd ACM SIGPLAN International Workshop on Type-Driven Development"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3240719.3241787","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3240719.3241787","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:33Z","timestamp":1750207413000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3240719.3241787"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,27]]},"references-count":24,"alternative-id":["10.1145\/3240719.3241787","10.1145\/3240719"],"URL":"https:\/\/doi.org\/10.1145\/3240719.3241787","relation":{},"subject":[],"published":{"date-parts":[[2018,9,27]]},"assertion":[{"value":"2018-09-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}