A Verified Compiler from Isabelle/HOL to CakeML

Thumbnail

Event details

Date 18.12.2018
Hour 15:0016:00
Location
Category Conferences - Seminars

By Lars Hupel, Technical University of Munich

Abstract
Many theorem provers can generate functional programs from definitions or proofs. However, this code generation needs to be trusted. Except for the HOL4 system, which has a proof producing code generator for a subset of ML. We go one step further and provide a verified compiler from Isabelle/HOL to CakeML. More precisely we combine a simple proof producing translation of recursion equations in Isabelle/HOL into a deeply embedded term language with a fully verified compilation chain to the target language CakeML, a verified functional programming language and an ecosystem of proofs and tools built around the language.

Bio
Lars Hupel is a PhD student at TU München in the field of logic and verification. His research focus is on techniques for verified code generation from theorem provers. Additionally, he has worked on formal treatments of Linux firewalls. A frequent conference speaker and co-founder of the Typelevel initiative, he is active in the open source community, particularly in Scala. He also enjoys programming in Haskell, Prolog, and Rust.

More information



 

Practical information

  • General public
  • Free

Contact

  • Host: Laboratory for Automated Reasoning and Analysis, http://lara.epfl.ch

Event broadcasted in

Share