{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:47Z","timestamp":1772164067108,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":43,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,6,11]],"date-time":"2018-06-11T00:00:00Z","timestamp":1528675200000},"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,6,11]]},"DOI":"10.1145\/3192366.3192372","type":"proceedings-article","created":{"date-parts":[[2018,6,12]],"date-time":"2018-06-12T08:16:01Z","timestamp":1528791361000},"page":"797-811","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Typed closure conversion for the calculus of constructions"],"prefix":"10.1145","author":[{"given":"William J.","family":"Bowman","sequence":"first","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[{"name":"Northeastern University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,6,11]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Summit on Advances in Programming Languages (SNAPL)","volume":"32","author":"Ahmed Amal","year":"2015","unstructured":"Amal Ahmed . 2015 . Verified Compilers for a Multi-language World . In Summit on Advances in Programming Languages (SNAPL) , Vol. 32 . Amal Ahmed. 2015. Verified Compilers for a Multi-language World. In Summit on Advances in Programming Languages (SNAPL), Vol. 32."},{"key":"e_1_3_2_2_2_1","volume-title":"Typed Closure Conversion Preserves Observational Equivalence. In International Conference on Functional Programming (ICFP).","author":"Ahmed Amal","year":"2008","unstructured":"Amal Ahmed and Matthias Blume . 2008 . Typed Closure Conversion Preserves Observational Equivalence. In International Conference on Functional Programming (ICFP). Amal Ahmed and Matthias Blume. 2008. Typed Closure Conversion Preserves Observational Equivalence. In International Conference on Functional Programming (ICFP)."},{"key":"e_1_3_2_2_3_1","volume-title":"An Equivalence-preserving CPS Translation Via Multi-language Semantics. In International Conference on Functional Programming (ICFP).","author":"Ahmed Amal","year":"2011","unstructured":"Amal Ahmed and Matthias Blume . 2011 . An Equivalence-preserving CPS Translation Via Multi-language Semantics. In International Conference on Functional Programming (ICFP). Amal Ahmed and Matthias Blume. 2011. An Equivalence-preserving CPS Translation Via Multi-language Semantics. In International Conference on Functional Programming (ICFP)."},{"key":"e_1_3_2_2_4_1","first-page":"4","article-title":"L3: A Linear Language with Locations","volume":"77","author":"Ahmed Amal","year":"2007","unstructured":"Amal Ahmed , Matthew Fluet , and Greg Morrisett . 2007 . L3: A Linear Language with Locations . Fundamenta Informaticae 77 , 4 (Dec. 2007). Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L3: A Linear Language with Locations. Fundamenta Informaticae 77, 4 (Dec. 2007).","journal-title":"Fundamenta Informaticae"},{"key":"e_1_3_2_2_5_1","volume-title":"CertiCoq: A Verified Compiler for Coq. In International Workshop on Coq for Programming Languages (CoqPL). http:\/\/www.cs.princeton.edu\/~appel\/papers\/certicoq-coqpl.pdf","author":"Anand Abhishek","year":"2017","unstructured":"Abhishek Anand , A. Appel , Greg Morrisett , Zoe Paraskevopoulou , Randy Pollack , Olivier Savary B\u00e9langer , Matthieu Sozeau , and Matthew Weaver . 2017 . CertiCoq: A Verified Compiler for Coq. In International Workshop on Coq for Programming Languages (CoqPL). http:\/\/www.cs.princeton.edu\/~appel\/papers\/certicoq-coqpl.pdf Abhishek Anand, A. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary B\u00e9langer, Matthieu Sozeau, and Matthew Weaver. 2017. CertiCoq: A Verified Compiler for Coq. In International Workshop on Coq for Programming Languages (CoqPL). http:\/\/www.cs.princeton.edu\/~appel\/papers\/certicoq-coqpl.pdf"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2701415"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792803.1792829"},{"key":"e_1_3_2_2_8_1","volume-title":"Formal Certification of Code-based Cryptographic Proofs. In Symposium on Principles of Programming Languages (POPL).","author":"Barthe Gilles","year":"2009","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , and Santiago Zanella-B\u00e9guelin . 2009 . Formal Certification of Code-based Cryptographic Proofs. In Symposium on Principles of Programming Languages (POPL). Gilles Barthe, Benjamin Gr\u00e9goire, and Santiago Zanella-B\u00e9guelin. 2009. Formal Certification of Code-based Cryptographic Proofs. In Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010000206149"},{"key":"e_1_3_2_2_10_1","volume-title":"CPS Translating Inductive and Coinductive Types. In Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM).","author":"Barthe Gilles","year":"2002","unstructured":"Gilles Barthe and Tarmo Uustalu . 2002 . CPS Translating Inductive and Coinductive Types. In Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM). Gilles Barthe and Tarmo Uustalu. 2002. CPS Translating Inductive and Coinductive Types. In Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM)."},{"key":"e_1_3_2_2_11_1","first-page":"02","article-title":"Proofs for Free: Parametricity for Dependent Types","volume":"22","author":"Jansson Patrik","year":"2012","unstructured":"Jean-philippe Bernardy, Patrik Jansson , and Ross Paterson . 2012 . Proofs for Free: Parametricity for Dependent Types . Journal of Functional Programming (JFP) 22 , 02 (March 2012). Jean-philippe Bernardy, Patrik Jansson, and Ross Paterson. 2012. Proofs for Free: Parametricity for Dependent Types. Journal of Functional Programming (JFP) 22, 02 (March 2012).","journal-title":"Journal of Functional Programming (JFP)"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018620"},{"key":"e_1_3_2_2_13_1","volume-title":"Noninterference for Free. In International Conference on Functional Programming (ICFP).","author":"William","unstructured":"William J. Bowman and Amal Ahmed. 2015 . Noninterference for Free. In International Conference on Functional Programming (ICFP). William J. Bowman and Amal Ahmed. 2015. Noninterference for Free. In International Conference on Functional Programming (ICFP)."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158110"},{"key":"e_1_3_2_2_16_1","volume-title":"Type-preserving Compilation of End-to-end Verification of Security Enforcement. In International Conference on Programming Language Design and Implementation (PLDI).","author":"Chen Juan","year":"2010","unstructured":"Juan Chen , Ravi Chugh , and Nikhil Swamy . 2010 . Type-preserving Compilation of End-to-end Verification of Security Enforcement. In International Conference on Programming Language Design and Implementation (PLDI). Juan Chen, Ravi Chugh, and Nikhil Swamy. 2010. Type-preserving Compilation of End-to-end Verification of Security Enforcement. In International Conference on Programming Language Design and Implementation (PLDI)."},{"key":"e_1_3_2_2_17_1","volume-title":"Symposium on Logic in Computer Science (LICS). https:\/\/hal.inria.fr\/inria-00076023","author":"Coquand Thierry","year":"1986","unstructured":"Thierry Coquand . 1986 . An Analysis of Girard's Paradox . In Symposium on Logic in Computer Science (LICS). https:\/\/hal.inria.fr\/inria-00076023 Thierry Coquand. 1986. An Analysis of Girard's Paradox. In Symposium on Logic in Computer Science (LICS). https:\/\/hal.inria.fr\/inria-00076023"},{"key":"e_1_3_2_2_18_1","volume-title":"Codifying Guarded Definitions with Recursive Schemes. In International Workshop on Types for Proofs and Programs (TYPES).","author":"Gim\u00e9nez Eduardo","year":"1995","unstructured":"Eduardo Gim\u00e9nez . 1995 . Codifying Guarded Definitions with Recursive Schemes. In International Workshop on Types for Proofs and Programs (TYPES). Eduardo Gim\u00e9nez. 1995. Codifying Guarded Definitions with Recursive Schemes. In International Workshop on Types for Proofs and Programs (TYPES)."},{"key":"e_1_3_2_2_19_1","volume-title":"On Strong Normalization of the Calculus of Constructions with Type-based Termination. In International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR).","author":"Gr\u00e9goire Benjamin","year":"2010","unstructured":"Benjamin Gr\u00e9goire and Jorge Luis Sacchini . 2010 . On Strong Normalization of the Calculus of Constructions with Type-based Termination. In International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). Benjamin Gr\u00e9goire and Jorge Luis Sacchini. 2010. On Strong Normalization of the Calculus of Constructions with Type-based Termination. In International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)."},{"key":"e_1_3_2_2_20_1","volume-title":"Deep Specifications and Certified Abstraction Layers. In Symposium on Principles of Programming Languages (POPL).","author":"Gu Ronghui","year":"2015","unstructured":"Ronghui Gu , J\u00e9r\u00e9mie Koenig , Tahina Ramananandro , Zhong Shao , Xiongnan (newman) Wu , Shu-chun Weng, Haozhong Zhang , and Yu Guo . 2015 . Deep Specifications and Certified Abstraction Layers. In Symposium on Principles of Programming Languages (POPL). Ronghui Gu, J\u00e9r\u00e9mie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan (newman) Wu, Shu-chun Weng, Haozhong Zhang, and Yu Guo. 2015. Deep Specifications and Certified Abstraction Layers. In Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_3_2_2_21_1","unstructured":"Ronghui Gu Zhong Shao Hao Chen Xiongnan (Newman) Wu Jieung Kim Vilhelm Sj\u00f6berg and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Symposium on Operating Systems Design and Implementation (OSDI). https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu   Ronghui Gu Zhong Shao Hao Chen Xiongnan (Newman) Wu Jieung Kim Vilhelm Sj\u00f6berg and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Symposium on Operating Systems Design and Implementation (OSDI) . https:\/\/www.usenix.org\/conference\/osdi16\/technical-sessions\/presentation\/gu"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_16"},{"key":"e_1_3_2_2_23_1","volume-title":"Howe","author":"Hook James G.","year":"1986","unstructured":"James G. Hook and Douglas J . Howe . 1986 . Impredicative Strong Existential Equivalent to Type:Type. Technical Report. Cornell University . http:\/\/hdl.handle.net\/1813\/6600 James G. Hook and Douglas J. Howe. 1986. Impredicative Strong Existential Equivalent to Type:Type. Technical Report. Cornell University. http:\/\/hdl.handle.net\/1813\/6600"},{"key":"e_1_3_2_2_24_1","volume-title":"Lightweight Verification of Separate Compilation. In Symposium on Principles of Programming Languages (POPL).","author":"Kang Jeehoon","year":"2016","unstructured":"Jeehoon Kang , Yoonseung Kim , Chung-Kil Hur , Derek Dreyer , and Viktor Vafeiadis . 2016 . Lightweight Verification of Separate Compilation. In Symposium on Principles of Programming Languages (POPL). Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, and Viktor Vafeiadis. 2016. Lightweight Verification of Separate Compilation. In Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_3_2_2_25_1","volume-title":"International Workshop on Computer Science Logic (CSL). https:\/\/hal.inria.fr\/hal-00730913","author":"Keller Chantal","year":"2012","unstructured":"Chantal Keller and Marc Lasson . 2012 . Parametricity in an Impredicative Sort . In International Workshop on Computer Science Logic (CSL). https:\/\/hal.inria.fr\/hal-00730913 Chantal Keller and Marc Lasson. 2012. Parametricity in an Impredicative Sort. In International Workshop on Computer Science Logic (CSL). https:\/\/hal.inria.fr\/hal-00730913"},{"key":"e_1_3_2_2_26_1","volume-title":"Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In International Workshop on Computer Science Logic (CSL).","author":"Neelakantan","unstructured":"Neelakantan R. Krishnaswami and Derek Dreyer. 2013 . Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In International Workshop on Computer Science Logic (CSL). Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In International Workshop on Computer Science Logic (CSL)."},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77390"},{"key":"e_1_3_2_2_29_1","volume-title":"A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday.","author":"McBride Conor","unstructured":"Conor McBride . 2016. I Got Plenty o' Nuttin '. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. Conor McBride. 2016. I Got Plenty o' Nuttin'. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday."},{"key":"e_1_3_2_2_30_1","volume-title":"Typed Closure Conversion. In Symposium on Principles of Programming Languages (POPL).","author":"Minamide Yasuhiko","year":"1996","unstructured":"Yasuhiko Minamide , Greg Morrisett , and Robert Harper . 1996 . Typed Closure Conversion. In Symposium on Principles of Programming Languages (POPL). Yasuhiko Minamide, Greg Morrisett, and Robert Harper. 1996. Typed Closure Conversion. In Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_3_2_2_31_1","volume-title":"The Implicit Calculus of Constructions. In International Conference on Typed Lambda Calculi and Applications (TLCA).","author":"Miquel Alexandre","year":"2001","unstructured":"Alexandre Miquel . 2001 . The Implicit Calculus of Constructions. In International Conference on Typed Lambda Calculi and Applications (TLCA). Alexandre Miquel. 2001. The Implicit Calculus of Constructions. In International Conference on Typed Lambda Calculi and Applications (TLCA)."},{"key":"e_1_3_2_2_32_1","volume-title":"Erasure and Polymorphism in Pure Type Systems. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS).","author":"Mishra-Linger Nathan","year":"2008","unstructured":"Nathan Mishra-Linger and Tim Sheard . 2008 . Erasure and Polymorphism in Pure Type Systems. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS)."},{"key":"e_1_3_2_2_33_1","unstructured":"Richard Nathan Mishra-linger. 2008. Irrelevance Polymorphism and Erasure in Type Theory. Ph.D. Dissertation. Portland State University. http:\/\/pdxscholar.library.pdx.edu\/cgi\/viewcontent.cgi?article=3678&context=open_access_etds  Richard Nathan Mishra-linger. 2008. Irrelevance Polymorphism and Erasure in Type Theory . Ph.D. Dissertation. Portland State University. http:\/\/pdxscholar.library.pdx.edu\/cgi\/viewcontent.cgi?article=3678&context=open_access_etds"},{"key":"e_1_3_2_2_34_1","volume-title":"Typed Closure Conversion for Recursively-defined Functions. Electronic Notes in Theoretical Computer Science 10 (June","author":"Morrisett Greg","year":"1998","unstructured":"Greg Morrisett and Robert Harper . 1998. Typed Closure Conversion for Recursively-defined Functions. Electronic Notes in Theoretical Computer Science 10 (June 1998 ), 230-241. Greg Morrisett and Robert Harper. 1998. Typed Closure Conversion for Recursively-defined Functions. Electronic Notes in Theoretical Computer Science 10 (June 1998), 230-241."},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/268946.268954"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784764"},{"key":"e_1_3_2_2_37_1","volume-title":"Fully Abstract Compilation Via Universal Embedding. In International Conference on Functional Programming (ICFP).","author":"New Max S.","year":"2016","unstructured":"Max S. New , William J. Bowman , and Amal Ahmed . 2016 . Fully Abstract Compilation Via Universal Embedding. In International Conference on Functional Programming (ICFP). Max S. New, William J. Bowman, and Amal Ahmed. 2016. Fully Abstract Compilation Via Universal Embedding. In International Conference on Functional Programming (ICFP)."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110276"},{"key":"e_1_3_2_2_39_1","unstructured":"Daniel Patterson and Amal Ahmed. 2017. Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. In Summit on Advances in Programming Languages (SNAPL).  Daniel Patterson and Amal Ahmed. 2017. Linking Types for Multi-Language Software: Have Your Cake and Eat It Too. In Summit on Advances in Programming Languages (SNAPL) ."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062347"},{"key":"e_1_3_2_2_41_1","volume-title":"European Symposium on Programming (ESOP).","author":"James","unstructured":"James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics . In European Symposium on Programming (ESOP). James T. Perconti and Amal Ahmed. 2014. Verifying an Open Compiler Using Multi-language Semantics. In European Symposium on Programming (ESOP)."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053469"},{"key":"e_1_3_2_2_43_1","volume-title":"Compositional CompCert. In Symposium on Principles of Programming Languages (POPL).","author":"Stewart Gordon","unstructured":"Gordon Stewart , Lennart Beringer , Santiago Cuellar , and Andrew W. Appel . 2015 . Compositional CompCert. In Symposium on Principles of Programming Languages (POPL). Gordon Stewart, Lennart Beringer, Santiago Cuellar, and Andrew W. Appel. 2015. Compositional CompCert. In Symposium on Principles of Programming Languages (POPL)."},{"key":"e_1_3_2_2_44_1","unstructured":"The Coq Development Team. 2017. The Coq Proof Assistant Reference Manual. https:\/\/web.archive.org\/web\/20170109225110\/https:\/\/coq.inria.fr\/doc\/Reference-Manual006.html  The Coq Development Team. 2017. The Coq Proof Assistant Reference Manual. https:\/\/web.archive.org\/web\/20170109225110\/https:\/\/coq.inria.fr\/doc\/Reference-Manual006.html"}],"event":{"name":"PLDI '18: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Philadelphia PA USA","acronym":"PLDI '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192372","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3192366.3192372","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:07:53Z","timestamp":1750198073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3192366.3192372"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,6,11]]},"references-count":43,"alternative-id":["10.1145\/3192366.3192372","10.1145\/3192366"],"URL":"https:\/\/doi.org\/10.1145\/3192366.3192372","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3296979.3192372","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2018,6,11]]},"assertion":[{"value":"2018-06-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}