{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:23:30Z","timestamp":1750307010304,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,1,22]],"date-time":"2013-01-22T00:00:00Z","timestamp":1358812800000},"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":[[2013,1,22]]},"DOI":"10.1145\/2428116.2428121","type":"proceedings-article","created":{"date-parts":[[2013,1,22]],"date-time":"2013-01-22T15:29:29Z","timestamp":1358868569000},"page":"13-24","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Compiling contextual objects"],"prefix":"10.1145","author":[{"given":"Francisco","family":"Ferreira","sequence":"first","affiliation":[{"name":"McGill University, Montr\u00e9al, PQ, Canada"}]},{"given":"Stefan","family":"Monnier","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Montr\u00e9al, Montr\u00e9al, PQ, Canada"}]},{"given":"Brigitte","family":"Pientka","sequence":"additional","affiliation":[{"name":"McGill University, Montr\u00e9al, PQ, Canada"}]}],"member":"320","published-online":{"date-parts":[[2013,1,22]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96712"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Andreas\n      Abel\n     and \n      Brigitte\n      Pientka\n    .\n  Higher-order dynamic pattern unification for dependent types and records\n  . In Luke Ong editor 10th International Conference on Typed Lambda Calculi and Applications (TLCA'11) Lecture Notes in Computer Science\n   (LNCS 6690) pages \n  10\n  --\n  26\n  . \n  Springer 2011\n  .   Andreas Abel and Brigitte Pientka. Higher-order dynamic pattern unification for dependent types and records. In Luke Ong editor 10th International Conference on Typed Lambda Calculi and Applications (TLCA'11) Lecture Notes in Computer Science (LNCS 6690) pages 10--26. Springer 2011.","DOI":"10.1007\/978-3-642-21691-6_5"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103705"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_2_1_5_1","first-page":"259","volume-title":"Joint International Conference and Symposium on Logic Programming","author":"Dowek Gilles","year":"1996","unstructured":"Gilles Dowek , Therese Hardin , Claude Kirchner , and Frank Pfenning . Unification via explicit substitutions: The case of higher-order patterns. In M. Maher, editor , Joint International Conference and Symposium on Logic Programming , pages 259 -- 273 . MIT Press , September 1996 . Gilles Dowek, Therese Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In M. Maher, editor, Joint International Conference and Symposium on Logic Programming, pages 259--273. MIT Press, September 1996."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.117"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507641"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411218"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_13_1","series-title":"Lecture Notes in Computer Science (LNCS 2646)","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-39185-1_12","volume-title":"Types for Proofs and Programs (TYPES'02)","author":"Letouzey Pierre","year":"2003","unstructured":"Pierre Letouzey . A new extraction for coq . In Herman Geuvers and Freek Wiedijk, editors, Types for Proofs and Programs (TYPES'02) , Lecture Notes in Computer Science (LNCS 2646) , pages 200 -- 219 . Springer , 2003 . Pierre Letouzey. A new extraction for coq. In Herman Geuvers and Freek Wiedijk, editors, Types for Proofs and Programs (TYPES'02), Lecture Notes in Computer Science (LNCS 2646), pages 200--219. Springer, 2003."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69407-6_39"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596571"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411304.1411311"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707790.1707792"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888270"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_2_1_21_1","volume-title":"Computation and Deduction","author":"Pfenning Frank","year":"2000","unstructured":"Frank Pfenning . Computation and Deduction . Cambridge University Press , 2000 . In preparation. Frank Pfenning. Computation and Deduction. Cambridge University Press, 2000. In preparation."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"crossref","unstructured":"Frank\n      Pfenning\n     and \n      Carsten\n      Sch\u00fcrmann\n    .\n  System description: Twelf -- a meta-logical framework for deductive systems\n  . In H. Ganzinger editor 16th International Conference on Automated Deduction (CADE-16) Lecture Notes in Artificial Intelligence\n   (LNAI 1632) pages \n  202\n  --\n  206\n  . \n  Springer 1999\n  .   Frank Pfenning and Carsten Sch\u00fcrmann. System description: Twelf -- a meta-logical framework for deductive systems. In H. Ganzinger editor 16th International Conference on Automated Deduction (CADE-16) Lecture Notes in Artificial Intelligence (LNAI 1632) pages 202--206. Springer 1999.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Brigitte\n      Pientka\n     and \n      Frank\n      Pfenning\n    .\n  Optimizing higher-order pattern unification\n  . In F. Baader editor 19th International Conference on Automated Deduction (CADE-19) Lecture Notes in Artificial Intelligence\n   (LNAI) 2741 pages \n  473\n  --\n  487\n  . \n  Springer-Verlag 2003\n  .  Brigitte Pientka and Frank Pfenning. Optimizing higher-order pattern unification. In F. Baader editor 19th International Conference on Automated Deduction (CADE-19) Lecture Notes in Artificial Intelligence (LNAI) 2741 pages 473--487. Springer-Verlag 2003.","DOI":"10.1007\/978-3-540-45085-6_40"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.120"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863575"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_8"},{"key":"e_1_3_2_1_31_1","volume-title":"1997 Workshop on Types in Compilation","author":"Shao Z.","year":"1997","unstructured":"Z. Shao . An overview of the FLINT\/ML compiler . In 1997 Workshop on Types in Compilation , 1997 . Z. Shao. An overview of the FLINT\/ML compiler. In 1997 Workshop on Types in Compilation, 1997."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289460"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944729"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006557"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034675.2034681"}],"event":{"name":"POPL '13: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"],"location":"Rome Italy","acronym":"POPL '13"},"container-title":["Proceedings of the 7th workshop on Programming languages meets program verification"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2428116.2428121","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2428116.2428121","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T08:49:01Z","timestamp":1750236541000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2428116.2428121"}},"subtitle":["bringing higher-order abstract syntax to programmers"],"short-title":[],"issued":{"date-parts":[[2013,1,22]]},"references-count":36,"alternative-id":["10.1145\/2428116.2428121","10.1145\/2428116"],"URL":"https:\/\/doi.org\/10.1145\/2428116.2428121","relation":{},"subject":[],"published":{"date-parts":[[2013,1,22]]},"assertion":[{"value":"2013-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}