Fri 25 Oct 2024 16:20 - 16:40 at Pasadena - Effects Chair(s): Jonathan Aldrich

Effect and coeffect tracking integrate many types of compile-time analysis, such as cost, liveness, or dataflow, directly into a languageā€™s type system. In this paper, we investigate the addition of effect and coeffect tracking to the type system of call-by-push-value (CBPV), a computational model useful in compilation for its isolation of effects and for its ability to cleanly express both call-by-name and call-by-value computations. Our main result is effect-and-coeffect soundness, which asserts that the type system accurately bounds the effects that the program may trigger during execution and accurately tracks the demands that the program may make on its environment. This result holds for two different dynamic semantics: a general one and one that is specialized for reasoning about resource usage. In particular, the second semantics discards the evaluation of unused values and pure computations, while ensuring that effectful computations are always evaluated, even if their results are not required. Our results have been mechanized using the Coq proof assistant.

Fri 25 Oct

Displayed time zone: Pacific Time (US & Canada) change

16:00 - 17:40
EffectsOOPSLA 2024 at Pasadena
Chair(s): Jonathan Aldrich Carnegie Mellon University
16:00
20m
Talk
Effect handlers for C via coroutines
OOPSLA 2024
Mario Alvarez-Picallo Huawei Research Centre, Teodoro Freund Huawei Research Centre, Dan Ghica Huawei, Sam Lindley The University of Edinburgh
DOI
16:20
20m
Talk
Effects and Coeffects in Call-By-Push-Value
OOPSLA 2024
Cassia Torczon University of Pennsylvania, Emmanuel Suarez Acevedo Cornell University, Shubh Agrawal University of Michigan, Joey Velez-Ginorio , Stephanie Weirich University of Pennsylvania
DOI
16:40
20m
Talk
Lexical Effect Handlers, Directly
OOPSLA 2024
Cong Ma University of Waterloo, Zhaoyi Ge University of Waterloo, Edward Lee University of Waterloo, Yizhou Zhang University of Waterloo
DOI
17:00
20m
Talk
Higher-Order Model Checking of Effect-Handling Programs with Answer-Type ModificationRemote
OOPSLA 2024
Taro Sekiyama National Institute of Informatics; SOKENDAI, Hiroshi Unno Tohoku University
DOI