A Verified Compiler from Isabelle/HOL to CakeML
Event details
Date | 18.12.2018 |
Hour | 15:00 › 16: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