Type inference in intuitionistic linear logic

11 years 8 months ago
Type inference in intuitionistic linear logic
We study the type checking and type inference problems for intuitionistic linear logic: given a System F typed λ-term, (i) for an alleged linear logic type, determine whether there exists a corresponding typing derivation in linear logic (type checking) (ii) provide a concise description of all possible corresponding linear logic typings (type inference). We solve these problems using a novel algorithmic type system for linear logic whose typing rules carry arithmetic side conditions describing essentially the nesting depth of (proof-net) boxes. By understanding these side conditions as unknowns we then reduce type inference to solving a system of arithmetic constraints. We show that these constraint systems fall into a tractable class hence leading to an efficient (polynomial-time) solution. There are two important restrictions: first, our source language is typed System F rather than untyped lambda calculus; this is necessary because type inference for System F is known to be und...
Patrick Baillot, Martin Hofmann
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where PPDP
Authors Patrick Baillot, Martin Hofmann
Comments (0)