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 OctDisplayed time zone: Pacific Time (US & Canada) change
16:00 - 17:40 | |||
16:00 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | Higher-Order Model Checking of Effect-Handling Programs with Answer-Type ModificationRemote OOPSLA 2024 DOI |