Safety at speed: In-place array algorithms from pure functional programs by safely re-using storage
We present a purely functional array programming language that offers safe, purely functional and crash-free in-place array transformations. The language supports high-level abstractions for pure and efficient array computations that fully support equational reasoning. We show how to execute selected parts of these computations \emph{safely} in-place, with the compiler guaranteeing that in-place execution does not change the computation’s result. Correctness is ensured by using an off-the-shelf-theorem prover to discharge safety conditions. Our main contribution is the idea of virtual copies for expressing re-use of arrays, and techniques for verifying their safety, which allow a pure language to include in-place transformations without weakening its transparency or reasoning power.
Sun 18 AugDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
15:20 - 16:40 | ArraysFHPNC at Reindeer Chair(s): Fritz Henglein Department of Computer Science, University of Copenhagen (DIKU) and Deon Digital | ||
15:20 25mTalk | Compiling Generalised Histograms for GPU (extended abstract) FHPNC Sune Hellfritzsch University of Copenhagen, Niels G. W. Serup DIKU, University of Copenhagen, Troels Henriksen University of Copenhagen, Denmark, Cosmin Oancea University of Copenhagen, Denmark | ||
15:46 26mTalk | Position-Dependent Arrays and Their Applicationfor High Performance Code Generation FHPNC Federico Pizzuti University of Edinburgh, Michel Steuwer University of Glasgow, Christophe Dubach University of Edinburgh Link to publication DOI Pre-print File Attached | ||
16:14 26mTalk | Safety at speed: In-place array algorithms from pure functional programs by safely re-using storage FHPNC Markus Aronsson , Koen Claessen Chalmers University of Technology, Mary Sheeran , Nicholas Smallbone Chalmers University of Technology, Sweden |