The speaker for this week’s seminar is Bas Spitters from Aarhus University. Please find the title and abstract below.

Title Peregrine: a verified middle-end for code generation from proof assistants

Abstract The code generation capabilities of proof assistants like Rocq, Agda, and Lean allow programs whose properties have been verified in the proof assistant to be extracted to industrial programming languages. This process is often trusted, with notable exceptions such as verified extraction from HOL4 and Isabelle/ HOL to CakeML and various verified extractions built around MetaRocq. Implementing and verifying an extraction pipeline remains an arduous task which one do es not want to repeat for every choice of proof assistant and target language. The Peregrine Project aims to simplify this process by providing a unified mi ddle-end for code generation, suitable for use with multiple proof assistants and target languages. We contribute Agda and Lean frontends to Peregrine, and a backend for CakeML extraction. Furthermore, we use MetaRocq’s verified erasure as a Rocq frontend and integrate several existing Rocq extraction pipelines as Peregrine backends for OCaml, C, WebAssembly, and Rust. In this way, we provide a unified, verified, and extensible middle-end between proof assistants and industrial programming languages. We have evaluated Peregrine on standard programming benchmarks and an industrial application.