A feasible algorithm for typing in Elementary Affine Logic

TL;DR

This paper introduces a new polynomial-time type inference algorithm for Elementary Affine Logic, enhancing efficiency for applications in complexity and optimal reduction.

Contribution

It presents a novel type inference algorithm for EAL* that operates in polynomial time, improving upon previous methods.

Findings

Type inference for EAL* is now polynomial time.

The algorithm is applicable to lambda-terms without sharing or polymorphism.

It advances the practical feasibility of using EAL in computational complexity.

Abstract

We give a new type inference algorithm for typing lambda-terms in Elementary Affine Logic (EAL), which is motivated by applications to complexity and optimal reduction. Following previous references on this topic, the variant of EAL type system we consider (denoted EAL*) is a variant without sharing and without polymorphism. Our algorithm improves over the ones already known in that it offers a better complexity bound: if a simple type derivation for the term t is given our algorithm performs EAL* type inference in polynomial time.