A Minimalistic Verified Bootstrapped Compiler (Proof Pearl) (CPP 2021 - Certified Programs and Proofs)

Write a Blog >>

Sun 17 - Fri 22 January 2021 Online

Track

CPP 2021

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Tue 19 Jan 2021 16:00 - 16:15 at CPP - Compilers and Interpreters Chair(s): Freek Wiedijk

Abstract

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.

Link to Preprint

http://www.cse.chalmers.se/~myreen/cpp2021-bootstrap-myreen.pdf

Long presentation

Short presentation

Time Zone

The program is currently displayed in (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna.

Use conference time zone: (GMT+01:00) Amsterdam, Berlin, Bern, Rome, Stockholm, ViennaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

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

A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)

Distinguished Paper Award

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Magnus O. Myreen

Chalmers University of Technology

Tracks

Co-hosted Conferences

Workshops

Co-hosted Symposiums

A Minimalistic Verified Bootstrapped Compiler (Proof Pearl)

Distinguished Paper Award

Program Display Configuration

Program Display Configuration

Tue 19 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Magnus O. Myreen

Chalmers University of Technology

Tue 19 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change