ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Sat 6 Apr 2019 17:00 - 17:30 at S1 (PERR) - IV

A typical transformation for optimizing recursive functions is to add an additional parameter called an accumulator, which holds the current result of the computation. The transformed function is usually tail-recursive, enabling the compiler to emit efficient code.

Typically, the optimized version of a function (i.e., the tail-recursive version) is simply assumed to be functionally equivalent to the original function. However, as we show here, this is not necessarily the case. We introduce a method for proving, in a semantics-based fashion, functional equivalence between recursive functions and their tail-recursive version, when the equivalence actually holds.

Our method requires a new technical development in the context of constrained term rewriting systems that we call defined functions, which can be used to mimic typical bigops in mathematics such as Σ, Π, ∀, etc. These defined functions can be then be used to define synchronization points in the two versions of the functions. Using unification modulo defined functions as a primitive, we define an algorithm for proving simulation between program configurations. Two-way simulation is used to show equivalence.

This paper presents work-in-progress results. Some of the technicalities involved are simplified in order to ensure a more straightforward presentation.

Sat 6 Apr
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:00: PERR - IV at S1 (PERR)
perr-2019-papers16:00 - 16:30
Moritz Kiefer, Mattias UlbrichKarlsruhe Institute of Technology
perr-2019-papers16:30 - 17:00
Carsten FuhsBirkbeck, University of London, Cynthia KopRadboud University Nijmegen, Naoki NishidaNagoya University
perr-2019-papers17:00 - 17:30
Stefan CiobacaAlexandru Ioan Cuza University of Iasi, Dorel Lucanu, Sebastian Buruiana