ICFP 2021
Sun 22 - Sat 28 August 2021
Mon 23 Aug 2021 19:15 - 19:30 at ICFP Talks - Session 2
Tue 24 Aug 2021 07:15 - 07:30 at ICFP Talks - Session 2

Compilers are difficult to write, and difficult to get right. Bahr and Hutton recently developed a new technique for calculating compilers directly from specifications of their correctness, which ensures that the resulting compilers are correct-by-construction. To date, however, this technique has only been applicable to source languages that are untyped. In this article, we show that moving to a dependently-typed setting allows us to naturally support typed source languages, ensure that all compilation components are type-safe, and make the resulting calculations easier to mechanically check using a proof assistant.

Mon 23 Aug

Displayed time zone: Seoul change

19:00 - 20:45
19:00
15m
Talk
Contextual Modal Types for Algebraic Effects and Handlers
Research Papers
Nikita Zyuzin IMDEA Software Institute, Aleksandar Nanevski IMDEA Software Institute
DOI Media Attached
19:15
15m
Talk
Calculating Dependently-Typed Compilers (Functional Pearl)
Research Papers
Mitchell Pickard University of Nottingham, Graham Hutton University of Nottingham
DOI Media Attached
19:30
15m
Talk
Reasoning about Effect Interaction by Fusion
Research Papers
Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London, UK
DOI Pre-print Media Attached
19:45
15m
Talk
Compositional Optimizations for CertiCoq
Research Papers
Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew Appel Princeton
DOI Media Attached
20:00
15m
Talk
Generalized Evidence Passing for Effect Handlers
Research Papers
Ningning Xie University of Hong Kong, Daan Leijen Microsoft Research
DOI Media Attached
20:15
15m
Talk
Deriving Efficient Program Transformations from Rewrite Rules
Research Papers
John M. Li Princeton University, Andrew W. Appel Princeton University
DOI Media Attached
20:30
15m
Talk
Algebras for Weighted Search
Research Papers
Oisín Kidney Imperial College London, Nicolas Wu Imperial College London, UK
DOI Media Attached

Tue 24 Aug

Displayed time zone: Seoul change

07:00 - 08:45
Session 2Research Papers at ICFP Talks
07:00
15m
Talk
Contextual Modal Types for Algebraic Effects and Handlers
Research Papers
Nikita Zyuzin IMDEA Software Institute, Aleksandar Nanevski IMDEA Software Institute
DOI Media Attached
07:15
15m
Talk
Calculating Dependently-Typed Compilers (Functional Pearl)
Research Papers
Mitchell Pickard University of Nottingham, Graham Hutton University of Nottingham
DOI Media Attached
07:30
15m
Talk
Reasoning about Effect Interaction by Fusion
Research Papers
Zhixuan Yang Imperial College London, Nicolas Wu Imperial College London, UK
DOI Pre-print Media Attached
07:45
15m
Talk
Compositional Optimizations for CertiCoq
Research Papers
Zoe Paraskevopoulou Northeastern University, John M. Li Princeton University, Andrew Appel Princeton
DOI Media Attached
08:00
15m
Talk
Generalized Evidence Passing for Effect Handlers
Research Papers
Ningning Xie University of Hong Kong, Daan Leijen Microsoft Research
DOI Media Attached
08:15
15m
Talk
Deriving Efficient Program Transformations from Rewrite Rules
Research Papers
John M. Li Princeton University, Andrew W. Appel Princeton University
DOI Media Attached
08:30
15m
Talk
Algebras for Weighted Search
Research Papers
Oisín Kidney Imperial College London, Nicolas Wu Imperial College London, UK
DOI Media Attached