{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:48:03Z","timestamp":1772164083647,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":28,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,8,30]],"date-time":"2015-08-30T00:00:00Z","timestamp":1440892800000},"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":[[2015,8,30]]},"DOI":"10.1145\/2804302.2804312","type":"proceedings-article","created":{"date-parts":[[2015,8,24]],"date-time":"2015-08-24T10:09:20Z","timestamp":1440410960000},"page":"35-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Formally proving a compiler transformation safe"],"prefix":"10.1145","author":[{"given":"Joachim","family":"Breitner","sequence":"first","affiliation":[{"name":"KIT, Germany"}]}],"member":"320","published-online":{"date-parts":[[2015,8,30]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.06.017"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9284-7"},{"key":"e_1_3_2_1_3_1","unstructured":"2\n   see  GHC commit 306d255  2 see GHC commit 306d255"},{"key":"e_1_3_2_1_4_1","volume-title":"Archive of Formal Proofs","author":"Breitner J.","year":"2013","unstructured":"J. Breitner . The correctness of Launchbury\u2019s natural semantics for lazy evaluation . Archive of Formal Proofs , Jan. 2013 . http:\/\/afp.sf.net\/ entries\/Launchbury.shtml. J. Breitner. The correctness of Launchbury\u2019s natural semantics for lazy evaluation. Archive of Formal Proofs, Jan. 2013. http:\/\/afp.sf.net\/ entries\/Launchbury.shtml."},{"key":"e_1_3_2_1_5_1","volume-title":"Archive of Formal Proofs","author":"Breitner J.","year":"2015","unstructured":"J. Breitner . The Safety of Call Arity . Archive of Formal Proofs , Feb. 2015 . http:\/\/afp.sf.net\/entries\/Call Arity.shtml. J. Breitner. The Safety of Call Arity. Archive of Formal Proofs, Feb. 2015. http:\/\/afp.sf.net\/entries\/Call Arity.shtml."},{"key":"e_1_3_2_1_6_1","series-title":"LNCS","first-page":"50","volume-title":"TFP\u201914","author":"Breitner J.","unstructured":"J. Breitner . Call Arity . In TFP\u201914 , volume 8843 of LNCS , pages 34\u2013 50 . Springer, 2015. J. Breitner. Call Arity. In TFP\u201914, volume 8843 of LNCS, pages 34\u201350. Springer, 2015."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_3_2_1_8_1","series-title":"LNCS","first-page":"225","volume-title":"LPAR\u201907","author":"Dargaye Z.","unstructured":"Z. Dargaye and X. Leroy . Mechanized Verification of CPS Transformations . In LPAR\u201907 , volume 4790 of LNCS , pages 211\u2013 225 . Springer, 2007. Z. Dargaye and X. Leroy. Mechanized Verification of CPS Transformations. In LPAR\u201907, volume 4790 of LNCS, pages 211\u2013225. Springer, 2007."},{"key":"e_1_3_2_1_9_1","volume-title":"System FC, as implemented in GHC","author":"Eisenberg R.","year":"2013","unstructured":"R. Eisenberg . System FC, as implemented in GHC , 2013 . URL https:\/\/github.com\/ghc\/ghc\/blob\/master\/docs\/core-spec\/ core-spec.pdf. R. Eisenberg. System FC, as implemented in GHC, 2013. URL https:\/\/github.com\/ghc\/ghc\/blob\/master\/docs\/core-spec\/ core-spec.pdf."},{"key":"e_1_3_2_1_10_1","volume-title":"Oct.","author":"Gammie P.","year":"2009","unstructured":"P. Gammie . The worker\/wrapper transformation. Archive of Formal Proofs , Oct. 2009 . http:\/\/afp.sf.net\/entries\/WorkerWrapper.shtml. P. Gammie. The worker\/wrapper transformation. Archive of Formal Proofs, Oct. 2009. http:\/\/afp.sf.net\/entries\/WorkerWrapper.shtml."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80284-1"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507667"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628142"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158618"},{"key":"e_1_3_2_1_18_1","series-title":"LNCS","first-page":"388","volume-title":"APLAS\u201912","author":"Leroy X.","unstructured":"X. Leroy . Mechanized semantics for compiler verification . In APLAS\u201912 , volume 7705 of LNCS , pages 386\u2013 388 . Springer, 2012. X. Leroy. Mechanized semantics for compiler verification. In APLAS\u201912, volume 7705 of LNCS, pages 386\u2013388. Springer, 2012."},{"key":"e_1_3_2_1_19_1","unstructured":"Invited talk.  Invited talk."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_23"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796806005995"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/976571.976576"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292547"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_1_25_1","first-page":"311","volume-title":"Glasgow Workshop on Functional Programming, Workshops in Computing Series","author":"Sands D.","unstructured":"D. Sands . Operational theories of improvement in functional languages (extended abstract) . In Glasgow Workshop on Functional Programming, Workshops in Computing Series , pages 298\u2013 311 . Springer, August 1991. D. Sands. Operational theories of improvement in functional languages (extended abstract). In Glasgow Workshop on Functional Programming, Workshops in Computing Series, pages 298\u2013311. Springer, August 1991."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535861"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002712"},{"key":"e_1_3_2_1_28_1","series-title":"CRPIT","first-page":"51","volume-title":"CATS\u201906","author":"Tian Y. H.","unstructured":"Y. H. Tian . Mechanically Verifying Correctness of CPS Compilation . In CATS\u201906 , volume 51 of CRPIT , pages 41\u2013 51 . ACS, 2006. Y. H. Tian. Mechanically Verifying Correctness of CPS Compilation. In CATS\u201906, volume 51 of CRPIT, pages 41\u201351. ACS, 2006."},{"key":"e_1_3_2_1_29_1","volume-title":"General Bindings and Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science, 8(2)","author":"Urban C.","year":"2012","unstructured":"C. Urban and C. Kaliszyk . General Bindings and Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science, 8(2) , 2012 .. C. Urban and C. Kaliszyk. General Bindings and Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science, 8(2), 2012.."},{"key":"e_1_3_2_1_30_1","volume-title":"Arity analysis","author":"Xu D. N.","year":"2005","unstructured":"D. N. Xu and S. Peyton Jones . Arity analysis , 2005 . Working Notes. Introduction Overview and Example From the Example\u2026 \u2026to the General Case Syntax and Semantics Semantics Arities and Eta-Expansion Arity Analyses Cardinality Analyses Abstract Cardinality Analysis Trace Tree Cardinality Analysis Co-Call Cardinality Analysis Call Arity, Concretely The Formalization in Isabelle The Formalization Effort The Formalization Gap Related Work Conclusion D. N. Xu and S. Peyton Jones. Arity analysis, 2005. Working Notes. Introduction Overview and Example From the Example\u2026 \u2026to the General Case Syntax and Semantics Semantics Arities and Eta-Expansion Arity Analyses Cardinality Analyses Abstract Cardinality Analysis Trace Tree Cardinality Analysis Co-Call Cardinality Analysis Call Arity, Concretely The Formalization in Isabelle The Formalization Effort The Formalization Gap Related Work Conclusion"}],"event":{"name":"ICFP'15: 20th ACM SIGPLAN International Conference on Functional Programming","location":"Vancouver BC Canada","acronym":"ICFP'15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 2015 ACM SIGPLAN Symposium on Haskell"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2804302.2804312","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2804302.2804312","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:07:10Z","timestamp":1750208830000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2804302.2804312"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,30]]},"references-count":28,"alternative-id":["10.1145\/2804302.2804312","10.1145\/2804302"],"URL":"https:\/\/doi.org\/10.1145\/2804302.2804312","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2887747.2804312","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,8,30]]},"assertion":[{"value":"2015-08-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}