ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Wed 14 Sep 2022 13:40 - 14:00 at Linhart - Programming and Reasoning About Effects Chair(s): William J. Bowman

Bahr and Hutton recently developed a new approach to calculating correct compilers directly from specifications of their correctness. However, the methodology only considers \emph{converging} behaviour of the source language, which means that the compiler could potentially produce arbitrary, erroneous code for source programs that diverge. In this article, we show how the methodology can naturally be extended to support the calculation of compilers that address both convergent and divergent behaviour \emph{simultaneously}, without the need for separate reasoning for each aspect. Our approach is based on the use of the partiality monad to make divergence explicit, together with the use of strong bisimilarity to support equational-style calculations, but also generalises to other forms of effect by changing the underlying monad.

Wed 14 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

13:40 - 15:20
Programming and Reasoning About EffectsICFP Papers and Events at Linhart
Chair(s): William J. Bowman University of British Columbia
13:40
20m
Talk
Monadic Compiler CalculationFunctional Pearl
ICFP Papers and Events
Patrick Bahr IT University of Copenhagen, Graham Hutton University of Nottingham, UK
DOI
14:00
20m
Talk
Formal Reasoning About Layered Monadic Interpreters
ICFP Papers and Events
Irene Yoon University of Pennsylvania, Yannick Zakowski Inria, Steve Zdancewic University of Pennsylvania
DOI
14:20
20m
Talk
Program Adverbs and Tlön EmbeddingsDistinguished PaperVirtual
ICFP Papers and Events
Yao Li Portland State University, Stephanie Weirich University of Pennsylvania
DOI Pre-print
14:40
20m
Talk
Flexible presentations of graded monads
ICFP Papers and Events
Shin-ya Katsumata National Institute of Informatics, Dylan McDermott Reykjavik University, Tarmo Uustalu Reykjavik University, Nicolas Wu Imperial College London
DOI
15:00
20m
Talk
Fusing Industry and Academia at GitHubExperience Report
ICFP Papers and Events
Patrick Thomson GitHub, Rob Rix GitHub, Inc., Tom Schrijvers KU Leuven, Nicolas Wu Imperial College London
DOI