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

Programming languages with algebraic effects often track the computations' effects using type-and-effect systems. In this paper, we propose to view an algebraic effect theory of a computation as a variable context; consequently, we propose to track algebraic effects of a computation with \emph{contextual modal types}. We develop ECMTT, a novel calculus which tracks algebraic effects by a contextualized variant of the modal $\Box$ (necessity) operator, that it inherits from Contextual Modal Type Theory (CMTT).

Whereas type-and-effect systems add effect annotations on top of a prior programming language, the effect annotations in ECMTT are inherent to the language, as they are managed by programming constructs corresponding to the logical introduction and elimination forms for the $\Box$ modality. Thus, the type-and-effect system of ECMTT is actually just a type system.

Our design obtains the properties of local soundness and completeness, and determines the operational semantics solely by $\beta$-reduction, as customary in other logic-based calculi. In this view, effect handlers arise naturally as a witness that one context (i.e., algebraic theory) can be reached from another, generalizing explicit substitutions from CMTT.

To the best of our knowledge, ECMTT is the first system to relate algebraic effects to modal types. We also see it as a step towards providing a correspondence in the style of Curry and Howard that may transfer a number of results from the fields of modal logic and modal type theory to that of algebraic effects.

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