Back to Direct Style: Typed and Tight

Explore a 15-minute conference talk from OOPSLA 2023 that delves into the intricacies of translating programs between continuation-passing style and direct style. Examine two languages, one in direct style and one in continuation-passing style, both featuring typing and abstract machine semantics. Learn about the type-preserving translations between these languages, their operational correspondence, and the preservation of semantics. Discover how the compositions of these translations behave, including their properties as syntactic inverses in certain contexts. Gain insights into the challenges and solutions for translating non-trivial control flow between continuation-passing and direct styles, and understand the implications for program compilation and logical interpretations in typed settings.