Fri 20 Jan 2023 13:30 - 13:55 at Avenue34 - Formal Methods in Compilation & Implementation Chair(s): Lindsey Kuper

The tail-recursion modulo \textit{cons} transformation can rewrite functions that are
not quite tail-recursive into a tail-recursive form that can be executed
efficiently. In this article we generalize tail recursion modulo \textit{cons} (TRMc)
to modulo \textit{contexts} (TRMC), and calculate a general TRMC algorithm from its
specification. We can instantiate our general algorithm by providing an
implementation of application and composition on abstract contexts, and showing
that our \textit{context} laws_ hold. We provide some known instantiations of TRMC,
namely modulo \textit{evaluation contexts} (CPS), and \textit{associative operations}, and further
instantiantions not so commonly associated with TRMC, such as
\textit{defunctionalized} evaluation contexts, \textit{monoids}, \textit{semirings},
\textit{exponents}, and \textit{cons products}. We study the modulo \textit{cons} instantiation in particular and prove
that an instantiation using Minamide's hole calculus is sound. We also
calculate a second instantiation in terms of the Perceus heap semantics to
precisely reason about the soundness of in-place update. While all previous
approaches to TRMc fail in the presence of non-linear control (for example
induced by call/cc, shift/reset or algebraic effect handlers), we can elegantly
extend the heap semantics to a hybrid approach which dynamically adapts to
non-linear control flow. We have a full implementation of hybrid TRMc in the
Koka language and our benchmark shows the TRMc transformed functions are always
as fast or faster than using manual alternatives.

Fri 20 Jan

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

13:30 - 14:45
Formal Methods in Compilation & ImplementationPOPL at Avenue34
Chair(s): Lindsey Kuper University of California at Santa Cruz
Tail Recursion Modulo Context: An Equational Approach
Daan Leijen Microsoft Research, Anton Lorenzen University of Edinburgh
Taking Back Control in an Intermediate Representation for GPU Computing
Vasileios Klimis Imperial College London, Jack Clark Imperial College London, Alan Baker Google, David Neto Google, John Wickerson Imperial College London, Alastair F. Donaldson Imperial College London; Google
Executing Microservice Applications on Serverless, Correctly
Konstantinos Kallas University of Pennsylvania, Haoran Zhang University of Pennsylvania, Rajeev Alur University of Pennsylvania, Sebastian Angel University of Pennsylvania; Microsoft Research, Vincent Liu University of Pennsylvania