Class Central is learner-supported. When you buy through links on our site, we may earn an affiliate commission.

YouTube

Shape-Constrained Array Programming with Size-Dependent Types

ACM SIGPLAN via YouTube

Overview

Explore a 43-minute video presentation from the FHPNC 2023 conference that introduces a dependent type system for enforcing array-size consistency in ML-style functional array languages. Delve into the innovative approach that aims to ensure shape-consistency at compile time while allowing complex transformations on array shapes, without the typical complexities associated with dependently typed languages. Learn how sizes can be arbitrary expressions with syntactical equality, fitting naturally into a scheme interpreting size-polymorphic functions as having implicit arguments. Discover the system's ability to automate book-keeping for tracking existential sizes, such as in array filtering scenarios. Gain insights into the formalization of a substantial subset of the presented type system, its soundness proof, and discussions on adapting it for real-world implementation, including type inference, within the Futhark programming language. Presented by Lubin Bailly, Troels Henriksen, and Martin Elsman from ENS, France, and the University of Copenhagen, Denmark, this talk offers valuable knowledge for those interested in type systems, parallel programming, and functional programming.

Syllabus

[FHPNC'23] Shape-Constrained Array Programming with Size-Dependent Types

Taught by

ACM SIGPLAN

Reviews

Start your review of Shape-Constrained Array Programming with Size-Dependent Types

Never Stop Learning.

Get personalized course recommendations, track subjects and courses with reminders, and more.

Someone learning on their laptop while sitting on the floor.