{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:22Z","timestamp":1775873542872,"version":"3.50.1"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T00:00:00Z","timestamp":1629331200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/P00587X\/1"],"award-info":[{"award-number":["EP\/P00587X\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2021,8,22]]},"abstract":"<jats:p>Compilers are difficult to write, and difficult to get right. Bahr and Hutton recently developed a new technique for calculating compilers directly from specifications of their correctness, which ensures that the resulting compilers are correct-by-construction. To date, however, this technique has only been applicable to source languages that are untyped. In this article, we show that moving to a dependently-typed setting allows us to naturally support typed source languages, ensure that all compilation components are type-safe, and make the resulting calculations easier to mechanically check using a proof assistant.<\/jats:p>","DOI":"10.1145\/3473587","type":"journal-article","created":{"date-parts":[[2021,8,19]],"date-time":"2021-08-19T10:44:29Z","timestamp":1629369869000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Calculating dependently-typed compilers (functional pearl)"],"prefix":"10.1145","volume":"5","author":[{"given":"Mitchell","family":"Pickard","sequence":"first","affiliation":[{"name":"University of Nottingham, UK"}]},{"given":"Graham","family":"Hutton","sequence":"additional","affiliation":[{"name":"University of Nottingham, UK"}]}],"member":"320","published-online":{"date-parts":[[2021,8,19]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Department of Computer Science","author":"Ager Mads Sig"},{"key":"e_1_2_2_2_1","unstructured":"Andrew Appel Lennart Beringer Adam Chlipala Benjamin Pearce Zhong Shao Stephanie Weirich and Steve Zdancewic. 2015. The Science of Deep Specification. https:\/\/deepspec.org\/  Andrew Appel Lennart Beringer Adam Chlipala Benjamin Pearce Zhong Shao Stephanie Weirich and Steve Zdancewic. 2015. The Science of Deep Specification. https:\/\/deepspec.org\/"},{"key":"e_1_2_2_3_1","volume-title":"Calculating Correct Compilers. Journal of Functional Programming, 25","author":"Bahr Patrick","year":"2015"},{"key":"e_1_2_2_4_1","volume-title":"Calculating Correct Compilers II: Return of the Register Machines. Journal of Functional Programming, 30","author":"Bahr Patrick","year":"2020"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173724"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250742"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110271"},{"key":"e_1_2_2_9_1","unstructured":"Conal Elliott. 2018. Calculating Compilers Categorically. https:\/\/tinyurl.com\/5de9xfm2  Conal Elliott. 2018. Calculating Compilers Categorically. https:\/\/tinyurl.com\/5de9xfm2"},{"key":"e_1_2_2_10_1","volume-title":"Reasoning with the Hermit: Tool Support for Equational Reasoning on GHC Core Programs. In Haskell Symposium.","author":"Farmer Andrew","year":"2015"},{"key":"e_1_2_2_11_1","volume-title":"Improving Haskell. In Proceedings of the Symposium on Trends in Functional Programming.","author":"Handley Martin","year":"2018"},{"key":"e_1_2_2_12_1","volume-title":"Compiling a 50-Year Journey. Journal of Functional Programming, 27","author":"Hutton Graham","year":"2017"},{"key":"e_1_2_2_13_1","volume-title":"The Verified CakeML Compiler Backend. Journal of Functional Programming, 29","author":"Tan Yong Kiam","year":"2019"},{"key":"e_1_2_2_14_1","volume-title":"Formal Verification of a Realistic Compiler. Communications of the ACM, 52, 7","author":"Leroy Xavier","year":"2009"},{"key":"e_1_2_2_15_1","unstructured":"2010. Haskell Language Report Simon Marlow (Ed.). Available on the web from: https:\/\/www.haskell.org\/definition\/haskell2010.pdf  2010. Haskell Language Report Simon Marlow (Ed.). Available on the web from: https:\/\/www.haskell.org\/definition\/haskell2010.pdf"},{"key":"e_1_2_2_16_1","unstructured":"Conor McBride. 2011. Ornamental Algebras Algebraic Ornaments. University of Strathclyde.  Conor McBride. 2011. Ornamental Algebras Algebraic Ornaments. University of Strathclyde."},{"key":"e_1_2_2_17_1","unstructured":"James Mckinna and Joel Wright. 2006. A Type-Correct Stack-Safe Provably Correct Expression Compiler in Epigram.  James Mckinna and Joel Wright. 2006. A Type-Correct Stack-Safe Provably Correct Expression Compiler in Epigram."},{"key":"e_1_2_2_18_1","unstructured":"Erik Meijer. 1992. Calculating Compilers. Ph.D. Dissertation. Katholieke Universiteit Nijmegen.  Erik Meijer. 1992. Calculating Compilers. Ph.D. Dissertation. Katholieke Universiteit Nijmegen."},{"key":"e_1_2_2_19_1","article-title":"Algebra of Programming in Agda: Dependent Types for Relational Program Derivation","volume":"19","author":"Jansson Patrik","year":"2009","journal-title":"Journal of Functional Programming"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236965"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158104"},{"key":"e_1_2_2_23_1","volume-title":"Proceedings of the ACM on Programming Languages, 5, POPL","author":"Rouvoet Arjen","year":"2021"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90056-J"},{"key":"e_1_2_2_25_1","volume-title":"Simon Peyton Jones, and Kevin Donnelly","author":"Sulzmann Martin","year":"2007"},{"key":"e_1_2_2_26_1","volume-title":"The Concatenate Vanishes","author":"Wadler Philip"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/357172.357179"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473587","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3473587","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:16Z","timestamp":1750195696000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3473587"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8,19]]},"references-count":26,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2021,8,22]]}},"alternative-id":["10.1145\/3473587"],"URL":"https:\/\/doi.org\/10.1145\/3473587","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,8,19]]},"assertion":[{"value":"2021-08-19","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}