Skip to content

Typechecking Linearity in Core

This is the tracking ticket for the work I'm doing for my Master thesis on typechecking linearity in Core.

UPDATE: A paper tackling this problem will be published at POPL26: "Lazy Linearity for a Core Functional Language". See also the announcement: https://alt-romes.github.io/posts/2025-11-26-lazy-linearity-popl26.html.

I'm currently finishing the soundness proof for the linear type system of a Core-like language, that annotates let and letrec bound variables as well as case binders with usage environments, as first proposed in the Minicore document.

I haven't (yet?) addressed GADTs and multiplicity coercions.

The (work in progress) dissertation motivates this issue and discusses the background, what I intend to do, and a tentative solution. Note that Chapter 3/4 are still much incomplete.

cc @monoidal

Edited by Rodrigo Mesquita
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information