Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020
Tue 16 Jun 2020 08:00 - 09:00 at PLMW live stream - Day 2 Morning Chair(s): Adrian Sampson

Compiler correctness is an old problem, with results stretching back beyond the last half-century and particularly impressive results such as CompCert over the last decade and a half. And yet, until quite recently, the theorems being proved were only about the compilation of whole programs, a theoretically appealing but practically unrealistic simplification since, in practice, compilers aren’t typically used to compile whole programs, but to compile components that are then linked with other components, even some written in other languages and compiled by different compilers.

There has been much recent work on “compositional” compiler correctness which tackles correct compilation of components. In this talk, I will survey recent results, explaining pros and cons of their different approaches to stating compiler correctness. These remarkably different ways of stating compiler correctness raises questions about what researchers even mean by a “compiler is correct.” I’ll briefly discuss a new framework for compositional compiler correctness (CCC) that helps us assess the relative strengths and weaknesses of recent results and helps provide insight into what we as a community should want from compiler correctness theorems of the future.

This talk will be live-streamed on YouTube here.

Tue 16 Jun

Displayed time zone: Pacific Time (US & Canada) change

07:00 - 09:00
Day 2 MorningPLMW@PLDI at PLMW live stream
Chair(s): Adrian Sampson Cornell University, USA

Live-stream link: https://youtu.be/ZLaps-g97CA

Q+A link: https://app.sli.do/event/h1ag9n8j

Mentoring talk: Research: It Takes a Village
Michael Carbin Massachusetts Institute of Technology, USA
Technical talk: Compositional Compiler Correctness
Amal Ahmed Northeastern University, USA