{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:59Z","timestamp":1772164019333,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":33,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,9,4]],"date-time":"2017-09-04T00:00:00Z","timestamp":1504483200000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"DARPA","award":["AFRL FA8750-15-2-0104"],"award-info":[{"award-number":["AFRL FA8750-15-2-0104"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,9,4]]},"DOI":"10.1145\/2951913.2951934","type":"proceedings-article","created":{"date-parts":[[2016,8,29]],"date-time":"2016-08-29T08:17:16Z","timestamp":1472458636000},"page":"311-324","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Constructive Galois connections: taming the Galois connection framework for mechanized metatheory"],"prefix":"10.1145","author":[{"given":"David","family":"Darais","sequence":"first","affiliation":[{"name":"University of Maryland, USA"}]},{"given":"David","family":"Van Horn","sequence":"additional","affiliation":[{"name":"University of Maryland, USA"}]}],"member":"320","published-online":{"date-parts":[[2016,9,4]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762189"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/248932"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/119830.119841"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781153"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38856-9_18"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_3"},{"key":"e_1_3_2_1_7_1","unstructured":"P. Cousot. Abstract interpretation."},{"key":"e_1_3_2_1_8_1","volume-title":"Calculational System Design","author":"Cousot P.","year":"1999","unstructured":"P. Cousot. The calculational design of a generic abstract interpreter. In M. Broy and R. Steinbr\u00fcggen, editors, Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam, 1999."},{"key":"e_1_3_2_1_9_1","volume-title":"Abstract interpretation","author":"Cousot P.","year":"2005","unstructured":"P. Cousot. MIT 16.399: Abstract interpretation, 2005."},{"key":"e_1_3_2_1_10_1","volume-title":"2nd International Symposium on Programming","author":"Cousot P.","year":"1976","unstructured":"P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In 2nd International Symposium on Programming, 1976."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/143165.143184"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2537850"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814308"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837670"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676966"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_20_1","volume-title":"ESOP 2016","author":"Malecha G.","year":"2016","unstructured":"G. Malecha and J. Bengtson. Extensible and efficient automation through reflective tactics. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016. Springer, 2016."},{"key":"e_1_3_2_1_21_1","volume-title":"Bibliopolis","author":"Martin-L\u00f6f P.","year":"1984","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_23"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69166-2_23"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_3_2_1_25_1","volume-title":"An abstract view of programming languages. Technical report","author":"Moggi E.","year":"1989","unstructured":"E. Moggi. An abstract view of programming languages. Technical report, Edinburgh University, 1989."},{"key":"e_1_3_2_1_26_1","volume-title":"Universit\u00e9 Paris VII","author":"Monniaux D.","year":"1998","unstructured":"D. Monniaux. R\u00e9alisation m\u00e9canis\u00e9e d\u2019interpr\u00e9teurs abstraits. Rapport de DEA, Universit\u00e9 Paris VII, 1998. French."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/555142"},{"key":"e_1_3_2_1_28_1","unstructured":"U. Norell. Towards a practical programming language based on dependent type theory. PhD thesis Department of Computer Science and Engineering Chalmers University of Technology SE-412 96 G\u00f6teborg Sweden Sept. 2007."},{"key":"e_1_3_2_1_29_1","unstructured":"D. Pichardie. Interpr\u00e9tation abstraite en logique intuitionniste: extraction d\u2019analyseurs Java certifi\u00e9s. PhD thesis Universit\u00e9 Rennes 2005."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31113-0_8"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491979"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389456"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946031.1946043"}],"event":{"name":"ICFP'16: ACM SIGPLAN International Conference on Functional Programming","location":"Nara Japan","acronym":"ICFP'16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2951913.2951934","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2951913.2951934","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2951913.2951934","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:18:27Z","timestamp":1763457507000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2951913.2951934"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,4]]},"references-count":33,"alternative-id":["10.1145\/2951913.2951934","10.1145\/2951913"],"URL":"https:\/\/doi.org\/10.1145\/2951913.2951934","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3022670.2951934","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,9,4]]},"assertion":[{"value":"2016-09-04","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}