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 Aug
15:20 - 16:40: FHPNC - Arrays at Reindeer Chair(s): Fritz HengleinDepartment of Computer Science, University of Copenhagen (DIKU) and Deon Digital | ||||||||||||||||||||||||||||||||||||||||||
15:20 - 15:45 Talk | Sune HellfritzschUniversity of Copenhagen, Niels G. W. SerupDIKU, University of Copenhagen, Troels HenriksenUniversity of Copenhagen, Denmark, Cosmin OanceaUniversity of Copenhagen, Denmark | |||||||||||||||||||||||||||||||||||||||||
15:46 - 16:13 Talk | Federico PizzutiUniversity of Edinburgh, Michel SteuwerUniversity of Glasgow, Christophe DubachUniversity of Edinburgh Link to publication DOI Pre-print File Attached | |||||||||||||||||||||||||||||||||||||||||
16:14 - 16:40 Talk | Markus Aronsson, Koen ClaessenChalmers University of Technology, Mary Sheeran, Nicholas SmallboneChalmers University of Technology, Sweden |