01 October 2020, 14:00, online

Speaker

James Wood, University of Strathclyde

Title

A Hygiene and Framework for Linear Calculi with Binding

Abstract

I will discuss work that Bob Atkey and myself are currently writing up. We propose a formally restricted but in practice permissive syntax of usage-annotated typing rules. This syntax guarantees that resulting calculi will have a notion of semantics that respects binding of variables. Included in this guarantee are completely generic renaming and substitution procedures on intrinsically typed terms. Usage annotations form a skew semiring, and act linearly in the sense of linear algebra. Each variable in the context is annotated by an element of the skew semiring, describing how it can be used. A context full of such annotations forms a vector. Typing rules can make requirements of their conclusion usage vector as a linear combination of premise vectors (0, +, and scaling by a scalar). The one special rule – the variable rule – requires its usage vector be a basis vector. This gives us enough to implement a wide range of linear calculi (in the sense of linear logic), including additives, multiplicatives, and exponentials. We believe our work can be of practical use to anyone working on simply typed linear and modal systems. Outside these bounds, we believe our work provides and justifies some simple heuristics for a linear calculus to be well behaved.