ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Wed 14 Sep 2022 11:30 - 11:50 at Linhart - Compilation Chair(s): Matija Pretnar

Purely functional programming languages pride themselves with reifying effects that are implicit in imperative languages into reusable and composable abstractions such as monads. This reification allows for more exact control over effects as well as the introduction of new or derived effects. However, despite libraries of more and more powerful abstractions over effectful operations being developed, syntactically the common do notation still lags behind equivalent imperative code it is supposed to mimic regarding verbosity and code duplication. In this paper, we explore extending do notation with other imperative language features that can be added to simplify monadic code: local mutation, early return, and iteration. We present formal translation rules that compile these features back down to purely functional code, show that the generated code can still be reasoned over using an implementation of the translation in the Lean 4 theorem prover, and formally prove the correctness of the translation rules relative to a simple static and dynamic semantics in Lean.

Wed 14 Sep

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

10:30 - 12:10
CompilationICFP Papers and Events at Linhart
Chair(s): Matija Pretnar University of Ljubljana, Slovenia
10:30
20m
Talk
Beyond Relooper: Recursive Translation of Unstructured Control Flow to Structured Control FlowFunctional Pearl
ICFP Papers and Events
Norman Ramsey Tufts University
DOI
10:50
20m
Talk
Automatically Deriving Control-Flow Graph Generators From Operational Semantics
ICFP Papers and Events
James Koppel Massachusetts Institute of Technology, USA, Jackson Kearl MIT, Armando Solar-Lezama Massachusetts Institute of Technology
DOI
11:10
20m
Talk
Analyzing Binding Extent in 3CPS
ICFP Papers and Events
Benjamin Quiring University of Maryland, Olin Shivers Northeastern University, USA, John Reppy University of Chicago, USA
DOI
11:30
20m
Talk
'do' Unchained: Embracing Local Imperativity in a Purely Functional LanguageFunctional Pearl
ICFP Papers and Events
Sebastian Ullrich Karlsruhe Institute of Technology, Leonardo de Moura Microsoft Research, n.n.
DOI
11:50
20m
Talk
ANF Preserves Dependent Types up to Extensional EqualityJFP Presentation
ICFP Papers and Events
Paulette Koronkevich University of British Columbia, Ramon Rakow University of British Columbia, Amal Ahmed Northeastern University, USA, William J. Bowman University of British Columbia