Typechecking Linearity in Core
This is the tracking ticket for the work I'm doing for my Master thesis on typechecking linearity in Core.
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