POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Wed 14 Jan 2026 11:45 - 12:10 at Nef - Functional Programming Chair(s): Alex Rice

Traditionally, in linearly typed languages, consuming a linear resource is synonymous with its syntactic occurrence in the program. However, under the lens of non-strict evaluation, linearity can be further understood semantically, where a syntactic occurrence of a resource does not necessarily entail using that resource when the program is executed. While this distinction has been largely unexplored, it turns out to be inescapable in Haskell's optimising compiler, which heavily rewrites the source program in ways that break syntactic linearity but preserve the program's semantics. We introduce Linear Core, a novel system which accepts the lazy semantics of linearity statically and is suitable for lazy languages such as the Core intermediate language of the Glasgow Haskell Compiler. We prove that Linear Core is sound, guaranteeing linear resource usage, and that multiple optimising transformations preserve linearity in Linear Core while failing to do so in Core. We have implemented Linear Core as a compiler plugin to validate the system against linearity-heavy libraries, including linear-base.

Wed 14 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

10:30 - 12:10
Functional Programming POPL at Nef
Chair(s): Alex Rice University of Edinburgh
10:30
25m
Talk
Domain-Theoretic Semantics for Functional Logic Programming
POPL
Eddie Jones University of Bristol, Samson Main University of Bristol, Celia Mengyue Li University of Bristol, Jonathan Marriott University of Bristol, Alex Kavvos University of Bristol
DOI
10:55
25m
Talk
Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
POPL
Michael Lee University of Cambridge, UK, Ningning Xie University of Toronto, Oleg Kiselyov Tohoku University, Jeremy Yallop University of Cambridge
DOI
11:20
25m
Talk
Hyperfunctions: Communicating Continuations
POPL
Donnacha Oisín Kidney Imperial College London, Nicolas Wu Imperial College London
DOI Pre-print
11:45
25m
Talk
Lazy Linearity for a Core Functional Language
POPL
Rodrigo Mesquita Well-Typed LLP, Bernardo Toninho Instituto Superior Técnico - University of Lisbon
DOI Pre-print