Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Wed 20 Jan 2021 16:30 - 16:40 at POPL-A - Compilers & Optimization

The polyhedral model is a high-level intermediate representation for loop nests that supports elegantly a great many loop optimizations. In a compiler, after polyhedral loop optimizations have been performed, it is necessary and difficult to regenerate sequential or parallel loop nests before continuing compilation. This paper reports on the formalization and proof of semantic preservation of such a code generator that produces sequential code from a polyhedral representation. The formalization and proofs are mechanized using the Coq proof assistant.

Wed 20 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:00
Compilers & OptimizationPOPL at POPL-A
16:00
10m
Talk
Fully Abstract from Static to Gradual
POPL
Koen Jacobs KU Leuven, Amin Timany Aarhus University, Dominique Devriese Vrije Universiteit Brussel
Link to publication DOI
16:10
10m
Talk
Intrinsically Typed Compilation with Nameless Labels
POPL
Arjen Rouvoet Delft University of Technology, Robbert Krebbers Radboud University Nijmegen, Eelco Visser Delft University of Technology
Link to publication DOI Pre-print
16:20
10m
Talk
A Verified Optimizer for Quantum CircuitsDistinguished Paper
POPL
Kesha Hietala University of Maryland, Robert Rand University of Chicago, Shih-Han Hung University of Maryland, USA, Xiaodi Wu University of Maryland, USA, Michael Hicks University of Maryland at College Park
Link to publication DOI
16:30
10m
Talk
Verified Code Generation for the Polyhedral Model
POPL
Nathanaël Courant INRIA, Xavier Leroy Collège de France
Link to publication DOI
16:40
10m
Talk
Formally Verified Speculation and Deoptimization in a JIT Compiler
POPL
Aurèle Barrière Univ Rennes, IRISA, Sandrine Blazy Univ Rennes, IRISA, Olivier Flückiger Northeastern University, David Pichardie Univ Rennes, ENS Rennes, IRISA, Jan Vitek Northeastern University / Czech Technical University
Link to publication DOI Pre-print
16:50
10m
Break
Break
POPL