Patrick Baillot and Martin Hofmann (2010)

# Type inference in intuitionistic linear logic

In: PPDP, pp. 219-230.

We study the type checking and type inference problems for intuitionistic linear logic: given a System F typed lambda-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$~$ 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 undecidable. Second, we assume that sharing is made explicit in the input, thus we do not try to$~$ automatically infer opportunities for sharing identical subterms. Relieving the latter restriction is left as a challenge for future work.

Document Actions