A Typed and Unified Reflection for Shift and Shift0
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 AugDisplayed time zone: Eastern Time (US & Canada) change
11:00 - 12:30 | |||
11:00 30mTalk | A Typed and Unified Reflection for Shift and Shift0 LOPSTR+PPDP | ||
11:30 30mTalk | 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 30mTalk | 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 | ||