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 15mTalk | A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)Distinguished Paper Award CPP Magnus O. MyreenChalmers University of Technology Pre-print Media Attached | ||
16:15 15mTalk | Lutsig: A Verified Verilog Compiler for Verified Circuit Development CPP Andreas LööwChalmers University of Technology Pre-print Media Attached | ||
16:30 15mTalk | 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 | ||
