POPL 2021 (series) / CPP 2021 (series) / Certified Programs and Proofs / A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)
A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)Distinguished Paper Award
This paper shows how a small verified bootstrapped compiler can be developed inside an interactive theorem prover (ITP). Throughout, emphasis is put on clarity and minimalism.
Tue 19 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 16:45: Compilers and InterpretersCPP at CPP Chair(s): Freek WiedijkRadboud University Nijmegen Streamed session: https://youtu.be/TVqCuMMTuos | |||
16:00 - 16:15 Talk | A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)Distinguished Paper Award CPP Magnus O. MyreenChalmers University of Technology Pre-print Media Attached | ||
16:15 - 16:30 Talk | Lutsig: A Verified Verilog Compiler for Verified Circuit Development CPP Andreas LööwChalmers University of Technology Pre-print Media Attached | ||
16:30 - 16:45 Talk | Towards Efficient and Verified Virtual Machines for Dynamic Languages CPP Martin DesharnaisUniversität der Bundeswehr München, Stefan BrunthalerUniversität der Bundeswehr München Pre-print Media Attached |