[LOPSTR+PPDP'26] A Typed and Unified Reflection for Shift and Shift0

A Typed and Unified Reflection for Shift and Shift0 (Video, LOPSTR+PPDP 2026) Yui Tamura, and Kenichi Asai (Ochanomizu University; Ochanomizu University) Abstract: 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. Presentation at the LOPSTR+PPDP 2026 symposium, August 27-29, 2026, https://icfp26.sigplan.org/home/lopstr-ppdp-2026 Sponsored by ACM SIGPLAN.