Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Tue 19 Jan 2021 16:00 - 16:15 at CPP - Compilers and Interpreters Chair(s): Freek Wiedijk

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

16:00 - 16:45
Compilers and InterpretersCPP at CPP
Chair(s): Freek WiedijkRadboud University Nijmegen

Streamed session: https://youtu.be/TVqCuMMTuos

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