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

YouTube

Soundly Handling Linearity - Combining Linear Types with Multi-Shot Effect Handlers

ACM SIGPLAN via YouTube

Overview

Explore a novel approach to combining linear types with multi-shot effect handlers in this 16-minute video presentation from POPL 2024. Delve into the concept of control-flow linearity as a solution to soundness issues in systems that mix linearity with effect handlers. Examine the formalization of this approach in a System F-style core calculus called Feff∘, featuring linear types, an effect type system, and effect handlers. Learn about the linearity-aware semantics used to prove the preservation of linear value integrity. Discover how this approach has been adapted to fix a long-standing soundness bug in the Links programming language. Explore the potential of control-flow linearity through the introduction of Qeff∘, an ML-style core calculus that uses qualified types for type inference without programmer annotations. Gain insights into overcoming practical limitations, including abstraction over linearity, linearity dependencies between type variables, and fine-grained control-flow linearity.

Syllabus

[POPL'24] Soundly Handling Linearity

Taught by

ACM SIGPLAN

Reviews

Start your review of Soundly Handling Linearity - Combining Linear Types with Multi-Shot Effect Handlers

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.