A new verified compiler backend for CakeML

Add to your list(s) Download to your calendar using vCal

• Magnus Myreen, Chalmers University, Sweden
• Thursday 18 August 2016, 15:00-16:00
• FW11.

If you have a question about this talk, please contact Dominic Mulligan.

**NOTE NON-STANDARD DATE, TIME, AND ROOM**

This talk will give an overview of the CakeML project and in particular report on a new compiler backend.

CakeML is a strict functional programming language in the style of Standard ML and OCaml. It has a verified implementation with verified parsing, type inference, and compilation.

We have recently developed and mechanically verified a new compiler backend for CakeML. Our new compiler features a sequence of intermediate languages that allows it to incrementally compile away high-level features and enables verification at the right levels of semantic detail. In this way, it resembles mainstream (unverified) compilers for strict functional languages. The compiler supports efficient curried multi-argument functions, configurable data representations, exceptions that unwind the call stack, register allocation, and more. The compiler targets several architectures: x86-64, ARMv6, ARMv8, MIPS -64, and RISC -V.

I will talk about the overall structure of the compiler, including its 12 intermediate languages, and explain how everything fits together. The talk focus particularly on the interaction between the verification of the register allocator and the garbage collector, and memory representations.

The CakeML project (https://cakeml.org/) is a collaboration between people at Data61 (Australia), Cambridge (UK), IHPC (Singapore), Kent (UK) and Chalmers (Sweden).

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• FW11
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.