Sat 29 Aug 2026 11:00 - 11:30 at IP137 Kelley - Morning Session 2

A reflection, a formal relationship between source and target calculi, strongly guarantees the correctness of program translations. Although reflection has been shown for delimited-control operators such as shift and shift0, existing reflections primarily focused on untyped calculi with a single control operator and their translations. As previous proofs for shift0 relied on formulations distinct from those for shift, a unified typed approach for both operators has yet to be formulated. In this paper, we present a unified reflection for typed shift and shift0. Recently, our group established a typed reflection for shift and reset. Based on this result, we demonstrate that the framework can be naturally extended with shift0. Our approach starts from a 2CPS interpreter, where both continuations and meta-continuations are explicitly passed. From this interpreter, we systematically derive a colon translation and a target language that avoids creating administrative redexes. Following previous work, we then establish the reflection. A crucial point in the proof is to precisely identify when a continuation is stored in the meta-continuation. The entire proof is formalized in Agda, assuming functional extensionality and postulating a certain structurally trivial rule required by the PHOAS representation. Our results clarify the operational semantics of delimited-control operators on a common foundation and would provide a basis for developing reflection for algebraic effects and handlers.

Sat 29 Aug

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

11:00 - 12:30
Morning Session 2LOPSTR+PPDP at IP137 Kelley
11:00
30m
Talk
A Typed and Unified Reflection for Shift and Shift0
LOPSTR+PPDP
Yui Tamura Ochanomizu University, Kenichi Asai Ochanomizu University
11:30
30m
Talk
Combining Small-Step and Big-Step Semantics to Verify Loop OptimizationsRemote
LOPSTR+PPDP
David Knothe FZI Research Center for Information Technology, Oliver Bringmann FZI Research Center for Information Technology
12:00
30m
Talk
Certified hardware for regexp matching: A rocq library and its workflowRemote
LOPSTR+PPDP
Julin Shaji Indian Institute of Technology Palakkad, Piyush Kurur Indian Institute of Technology Palakkad, Sandeep Chandran Indian Institute of Technology Palakkad