Skip to main content
Kent Academic Repository

PureCake: A verified compiler for a lazy functional language

Kanabar, Hrutvik, Vivien, Samuel, Abrahamsson, Oskar, Myreen, Magnus O., Norrish, Michael, Pohjola, Johannes Åman, Zanetti, Riccardo (2023) PureCake: A verified compiler for a lazy functional language. Proceedings of the ACM on Programming Languages, 7 (PLDI). pp. 952-976. E-ISSN 2475-1421. (doi:10.1145/3591259) (KAR id:101697)


We present PureCake, a mechanically-verified compiler for PureLang, a lazy, purely functional programming language with monadic effects. PureLang syntax is Haskell-like and indentation-sensitive, and its constraint-based Hindley-Milner type system guarantees safe execution. We derive sound equational reasoning principles over its operational semantics, dramatically simplifying some proofs. We prove end-to-end correctness for the compilation of PureLang down to machine code---the first such result for any lazy language---by targeting CakeML and composing with its verified compiler. Multiple optimisation passes are necessary to handle realistic lazy idioms effectively. We develop PureCake entirely within the HOL4 interactive theorem prover.

Item Type: Article
DOI/Identification number: 10.1145/3591259
Uncontrolled keywords: safety, risk, reliability and quality; Software; compiler verification, Haskell, interactive theorem proving, HOL4
Subjects: Q Science > QA Mathematics (inc Computing science)
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
SWORD Depositor: JISC Publications Router
Depositing User: JISC Publications Router
Date Deposited: 11 Aug 2023 14:17 UTC
Last Modified: 14 Aug 2023 13:40 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.