| 1. |
- Abrahamsson, Oskar, 1986, et al.
(författare)
-
Proof-Producing Synthesis of CakeML from Monadic HOL Functions
- 2020
-
Ingår i: Journal of Automated Reasoning. - : Springer Science and Business Media LLC. - 0168-7433 .- 1573-0670. ; 64:7, s. 1287-1306
-
Tidskriftsartikel (refereegranskat)abstract
- We introduce an automatic method for producing stateful ML programs together with proofs of correctness from monadic functions in HOL. Our mechanism supports references, exceptions, and I/O operations, and can generate functions manipulating local state, which can then be encapsulated for use in a pure context. We apply this approach to several non-trivial examples, including the instruction encoder and register allocator of the otherwise pure CakeML compiler, which now benefits from better runtime performance. This development has been carried out in the HOL4 theorem prover.
|
|
| 2. |
- Kanabar, Hrutvik, et al.
(författare)
-
PureCake: A Verified Compiler for a Lazy Functional Language
- 2023
-
Ingår i: Proceedings of the ACM on Programming Languages. - 2475-1421. ; 7
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 3. |
- Kanabar, Hrutvik, et al.
(författare)
-
Taming an Authoritative Armv8 ISA Specification: L3 Validation and CakeML Compiler Verification
- 2022
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. ; 237
-
Konferensbidrag (refereegranskat)abstract
- Machine-readable specifications for the Armv8 instruction set architecture have become publicly available as part of Arm's release processes, providing an official and unambiguous source of truth for the semantics of Arm instructions. To date, compiler and machine code verification efforts have made use of unofficial theorem-proving-friendly specifications of Armv8, e.g. CakeML uses an L3-based specification. The validity of these verification efforts hinges upon their unofficial ISA specifications being valid with respect to the official Arm specification. Leveraging the Sail language ecosystem, we bridge this validation gap by formally verifying that an L3-based specification simulates the official Arm specification using the HOL4 interactive theorem prover. We exercise this simulation by proving a novel compiler correctness result for CakeML with respect to Arm's official specification of the Armv8.6 A-class instruction set.
|
|
| 4. |
- Kanabar, Hrutvik, et al.
(författare)
-
Verified Inlining and Specialisation for PureCake
- 2024
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - 1611-3349 .- 0302-9743. ; 14577 LNCS, s. 275-301
-
Konferensbidrag (refereegranskat)abstract
- Inlining is a crucial optimisation when compiling functional programming languages. This paper describes how we have implemented and verified function inlining and loop specialisation for PureCake, a verified compiler for a Haskell-like (purely functional, lazy) programming language. A novel aspect of our formalisation is that we justify inlining by pushing and pulling -bindings. All of our work has been mechanised in the HOL4 interactive theorem prover.
|
|
