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

Effect handlers can be composed by applying them sequentially, each handling some operations and leaving other operations uninterpreted in the syntax tree. However, the semantics of composed handlers can be subtle—it is well known that different orders of composing handlers can lead to drastically different semantics. Determining the correct order of composition is a non-trivial task.

To alleviate this problem, this paper presents a systematic way of deriving sufficient conditions on handlers for their composite to correctly handle combinations, such as the sum and the tensor, of the effect theories separately handled. These conditions are solely characterised by the clauses for relevant operations of the handlers, and are derived by fusing two handlers into one using a form of fold/build fusion and continuation-passing style transformation.

As case studies, the technique is applied to commutative and distributive interaction of handlers to obtain a series of results about the interaction of common handlers: (a) equations respected by each handler are preserved after handler composition; (b) handling mutable state before any handler gives rise to a semantics in which state operations are commutative with any operations from the latter handler; (c) handling the writer effect and mutable state in either order gives rise to a correct handler of the commutative combination of these two theories.

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 W. Appel Princeton
DOI Media Attached
20:00
15m
Talk
Generalized Evidence Passing for Effect Handlers
Research Papers
Ningning Xie University of Toronto, 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 W. Appel Princeton
DOI Media Attached
08:00
15m
Talk
Generalized Evidence Passing for Effect Handlers
Research Papers
Ningning Xie University of Toronto, 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