ICFP/SPLASH 2025 (series) / SPLASH 2025 (series) / OOPSLA /
Adequacy for Algebraic Effects Revisited
We prove an adequacy theorem for a general class of algebraic effects, including infinitary ones. Our theorem targets a version of call-by-push-value, so that it applies to many possible evaluation mechanisms, including call-by-value. Our calculus is given an operational semantics based on interaction trees, as well as a denotational semantics based on monad algebras. We prove our main adequacy result, viz. that denotational equivalence implies observational equivalence, using a traditional logical relations argument.
Fri 17 OctDisplayed time zone: Perth change
Fri 17 Oct
Displayed time zone: Perth change
13:45 - 15:30 | |||
13:45 15mTalk | A complete formal semantics of eBPF instruction set architecture for Solana OOPSLA Shenghao Yuan Zhejiang University, Zhuoruo Zhang Zhejiang University, Jiayi Lu Zhejiang University, David Sanan Singapore Institute of Technology, Rui Chang Zhejiang University, Yongwang Zhao Zhejiang University | ||
14:00 15mTalk | Adequacy for Algebraic Effects Revisited OOPSLA Alex Kavvos University of Bristol | ||
14:15 15mTalk | A Mechanized Semantics for Dataflow Circuits OOPSLA Tony Law Univ Rennes, Inria, CNRS, IRISA, Delphine Demange Univ Rennes, Inria, CNRS, IRISA, Sandrine Blazy University of Rennes | ||
14:30 15mTalk | Dynamic Wind for Effect Handlers OOPSLA David Voigt University of Tübingen, Philipp Schuster University of Tübingen, Jonathan Immanuel Brachthäuser University of Tübingen Pre-print | ||
14:45 15mTalk | React-tRace: A Semantics for Understanding React Hooks OOPSLA Jay Lee Seoul National University, Joongwon Ahn Seoul National University, Kwangkeun Yi Seoul National University Link to publication DOI | ||
15:00 15mTalk | Semantics of Sets of Programs OOPSLA Jinwoo Kim University of Wisconsin-Madison; Seoul National University, Shaan Nagy University of Wisconsin-Madison, Thomas Reps University of Wisconsin-Madison, Loris D'Antoni University of California at San Diego | ||
15:15 15mTalk | Zero-Overhead Lexical Effect Handlers OOPSLA Cong Ma University of Waterloo, Zhaoyi Ge University of Waterloo, Max Jung University of Waterloo, Yizhou Zhang University of Waterloo | ||
