Write a Blog >>
PLDI 2021
Sun 20 - Sat 26 June 2021 PLDI
Mon 21 Jun 2021 10:45 - 11:15 at ARRAY - Session 1 (principles) Chair(s): Artjoms Šinkarovs

We present a type system for expressing size constraints on array-typed function parameters in an ML-style type system. The goal is to detect shape mismatches at compile-time, while being simpler than full dependent types. The main restrictions is that the only terms that can occur in types are array sizes, and syntactically they must be variables or constants. For those programs where this is not sufficient, we support a form of existential types, with the type system automatically managing the requisite book-keeping. We formalise a large subset of the type system in a small core language, which we prove sound. We also present an integration of the type system in the high-performance parallel functional language Futhark, and show on a collection of 44 representative programs that the restrictions in the type system are not too problematic in practice.

Mon 21 Jun

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

09:00 - 11:45
Session 1 (principles)ARRAY at ARRAY
Chair(s): Artjoms Šinkarovs Heriot-Watt University, UK
Day opening
Welcome and opening
Jeremy Gibbons Department of Computer Science, University of Oxford
Towards size-dependent types for array programming
Troels Henriksen University of Copenhagen, Denmark, Martin Elsman University of Copenhagen, Denmark
Padding in the Mathematics of Arrays
Benjamin Chetioui University of Bergen, Norway, Ole Abusdal Western Norway University of Applied Sciences, Magne Haveraaen University of Bergen, Norway, Jaakko Järvi University of Turku, Lenore Mullin University at Albany, SUNY