{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,17]],"date-time":"2026-01-17T19:50:14Z","timestamp":1768679414406,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,16]],"date-time":"2017-01-16T00:00:00Z","timestamp":1484524800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["320571"],"award-info":[{"award-number":["320571"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K020218\/1,EP\/M016951\/1"],"award-info":[{"award-number":["EP\/K020218\/1,EP\/M016951\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1,16]]},"DOI":"10.1145\/3018610.3018613","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T21:20:29Z","timestamp":1482441629000},"page":"195-207","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":33,"title":["Type-and-scope safe programs and their proofs"],"prefix":"10.1145","author":[{"given":"Guillaume","family":"Allais","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}]},{"given":"James","family":"Chapman","sequence":"additional","affiliation":[{"name":"University of Strathclyde, UK"}]},{"given":"Conor","family":"McBride","sequence":"additional","affiliation":[{"name":"University of Strathclyde, UK"}]},{"given":"James","family":"McKinna","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}]}],"member":"320","published-online":{"date-parts":[[2017,1,16]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"MSFP 2014","author":"Abel A.","year":"2014","unstructured":"A. Abel and J. Chapman . Normalization by evaluation in the delay monad . MSFP 2014 , 2014 . A. Abel and J. Chapman. Normalization by evaluation in the delay monad. MSFP 2014, 2014."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429075"},{"key":"e_1_3_2_1_3_1","first-page":"468","volume-title":"CSL","author":"Allais G.","unstructured":"G. Allais , J. Chapman , C. McBride , and J. McKinna . Type- and-scope safe programs and their proofs \u2013 agda formalization. Also from github https:\/\/github.com\/gallais\/ type-scope-semantics. T. Altenkirch and B. Reus. Monadic presentations of lambda terms using generalized inductive types . In CSL , pages 453\u2013 468 . Springer, 1999. G. Allais, J. Chapman, C. McBride, and J. McKinna. Type- and-scope safe programs and their proofs \u2013 agda formalization. Also from github https:\/\/github.com\/gallais\/ type-scope-semantics. T. Altenkirch and B. Reus. Monadic presentations of lambda terms using generalized inductive types. In CSL, pages 453\u2013468. Springer, 1999."},{"key":"e_1_3_2_1_4_1","first-page":"199","volume-title":"LNCS","volume":"530","author":"Altenkirch T.","unstructured":"T. Altenkirch , M. Hofmann , and T. Streicher . Categorical reconstruction of a reduction free normalization proof . In LNCS , volume 530 , pages 182\u2013 199 . Springer, 1995. T. Altenkirch, M. Hofmann, and T. Streicher. Categorical reconstruction of a reduction free normalization proof. In LNCS, volume 530, pages 182\u2013199. Springer, 1995."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_3_2_1_6_1","first-page":"106","volume-title":"TLCA","author":"Berger U.","unstructured":"U. Berger . Program extraction from normalization proofs . In TLCA , pages 91\u2013 106 . Springer, 1993. U. Berger. Program extraction from normalization proofs. In TLCA, pages 91\u2013106. Springer, 1993."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500577"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809007205"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411203.1411226"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019964114625"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129596002150"},{"key":"e_1_3_2_1_13_1","first-page":"99","volume-title":"IFL","author":"Danielsson N. A.","unstructured":"N. A. Danielsson and U. Norell . Parsing mixfix operators . In IFL , pages 80\u2013 99 . Springer, 2011. N. A. Danielsson and U. Norell. Parsing mixfix operators. In IFL, pages 80\u201399. Springer, 2011."},{"key":"e_1_3_2_1_14_1","first-page":"411","volume-title":"Partial Evaluation","author":"Danvy O.","unstructured":"O. Danvy . Type-directed partial evaluation . In Partial Evaluation , pages 367\u2013 411 . Springer, 1999. O. Danvy. Type-directed partial evaluation. In Partial Evaluation, pages 367\u2013411. Springer, 1999."},{"key":"e_1_3_2_1_15_1","volume-title":"Tagless and typeful normalization by evaluation using generalized algebraic data types","author":"Danvy O.","year":"2013","unstructured":"O. Danvy , C. Keller , and M. Puech . Tagless and typeful normalization by evaluation using generalized algebraic data types . 2013 . O. Danvy, C. Keller, and M. Puech. Tagless and typeful normalization by evaluation using generalized algebraic data types. 2013."},{"key":"e_1_3_2_1_16_1","first-page":"392","volume-title":"Indagationes Mathematicae","author":"de Bruijn N. G.","unstructured":"N. G. de Bruijn . Lambda Calculus notation with nameless dummies . In Indagationes Mathematicae , volume 75 , pages 381\u2013 392 . Elsevier, 1972. N. G. de Bruijn. Lambda Calculus notation with nameless dummies. In Indagationes Mathematicae, volume 75, pages 381\u2013392. Elsevier, 1972."},{"key":"e_1_3_2_1_17_1","first-page":"6","article-title":"Inductive sets and families in Martin-L\u00f6f\u2019s type theory and their set-theoretic semantics","volume":"2","author":"Dybjer P.","year":"1991","unstructured":"P. Dybjer . Inductive sets and families in Martin-L\u00f6f\u2019s type theory and their set-theoretic semantics . Logical Frameworks , 2 : 6 , 1991 . P. Dybjer. Inductive sets and families in Martin-L\u00f6f\u2019s type theory and their set-theoretic semantics. Logical Frameworks, 2:6, 1991.","journal-title":"Logical Frameworks"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2430532.2364522"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2611429.2617811"},{"key":"e_1_3_2_1_20_1","unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. 1972.  J.-Y. Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. 1972."},{"key":"e_1_3_2_1_21_1","volume-title":"LFCS","author":"Goguen H.","year":"1997","unstructured":"H. Goguen and J. McKinna . Candidates for substitution . LFCS , Edinburgh Techreport , 1997 . H. Goguen and J. McKinna. Candidates for substitution. LFCS, Edinburgh Techreport, 1997."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178053"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/242224.242477"},{"key":"e_1_3_2_1_24_1","first-page":"96","volume-title":"AFP Summer School","author":"Hughes J.","unstructured":"J. Hughes . The design of a pretty-printing library . In AFP Summer School , pages 53\u2013 96 . Springer, 1995. J. Hughes. The design of a pretty-printing library. In AFP Summer School, pages 53\u201396. Springer, 1995."},{"key":"e_1_3_2_1_25_1","volume-title":"Associativity for free! http:\/\/thread.gmane. org\/gmane.comp.lang.agda\/3259","author":"Jeffrey A.","year":"2011","unstructured":"A. Jeffrey . Associativity for free! http:\/\/thread.gmane. org\/gmane.comp.lang.agda\/3259 , 2011 . A. Jeffrey. Associativity for free! http:\/\/thread.gmane. org\/gmane.comp.lang.agda\/3259, 2011."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578854.2503786"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_3_2_1_28_1","volume-title":"The Coq proof assistant reference manual","author":"The Coq","year":"2004","unstructured":"The Coq development team. The Coq proof assistant reference manual , 2004 . The Coq development team. The Coq proof assistant reference manual, 2004."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_30_1","unstructured":"J. C. Mitchell. Foundations for programming languages volume 1. MIT press 1996.   J. C. Mitchell. Foundations for programming languages volume 1. MIT press 1996."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90067-V"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_3_2_1_33_1","first-page":"266","volume-title":"AFP Summer School","author":"Norell U.","unstructured":"U. Norell . Dependently typed programming in Agda . In AFP Summer School , pages 230\u2013 266 . Springer, 2009. U. Norell. Dependently typed programming in Agda. In AFP Summer School, pages 230\u2013266. Springer, 2009."},{"key":"e_1_3_2_1_34_1","volume-title":"abstraction and parametric polymorphism","author":"Reynolds J. C.","year":"1983","unstructured":"J. C. Reynolds . Types , abstraction and parametric polymorphism . 1983 . J. C. Reynolds. Types, abstraction and parametric polymorphism. 1983."},{"key":"e_1_3_2_1_35_1","first-page":"36","volume-title":"TFP","author":"Svenningsson J.","unstructured":"J. Svenningsson and E. Axelsson . Combining deep and shallow embedding for EDSL . In TFP , pages 21\u2013 36 . Springer, 2013. J. Svenningsson and E. Axelsson. Combining deep and shallow embedding for EDSL. In TFP, pages 21\u201336. Springer, 2013."},{"key":"e_1_3_2_1_36_1","first-page":"243","volume-title":"Cornerstones of Computing","author":"Wadler P.","year":"2003","unstructured":"P. Wadler . A prettier printer. The Fun of Programming , Cornerstones of Computing , pages 223\u2013 243 , 2003 . P. Wadler. A prettier printer. The Fun of Programming, Cornerstones of Computing, pages 223\u2013243, 2003."},{"key":"e_1_3_2_1_37_1","first-page":"85","volume":"285","author":"Wiedijk F.","year":"2012","unstructured":"F. Wiedijk . Pollack-inconsistency. ENTCS , 285 : 85 \u2013 100 , 2012 . F. Wiedijk. Pollack-inconsistency. ENTCS, 285:85\u2013100, 2012.","journal-title":"Pollack-inconsistency. ENTCS"}],"event":{"name":"CPP '17: Certified Proofs and Programs","location":"Paris France","acronym":"CPP '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018613","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3018610.3018613","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:23:58Z","timestamp":1750220638000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3018610.3018613"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,16]]},"references-count":36,"alternative-id":["10.1145\/3018610.3018613","10.1145\/3018610"],"URL":"https:\/\/doi.org\/10.1145\/3018610.3018613","relation":{},"subject":[],"published":{"date-parts":[[2017,1,16]]},"assertion":[{"value":"2017-01-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}