A feasible algorithm for typing in Elementary Affine Logic.

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 where sharing is restricted to variables 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 in the size of the derivation.

Data and Resources

Additional Info

Field Value
Source 7th International Conference on Typed Lambda Calculi and Applications (TLCA 2005)
Author Baillot, Patrick, Terui, Kazushige
Maintainer CCSD
Last Updated May 10, 2026, 07:11 (UTC)
Created May 10, 2026, 07:11 (UTC)
Identifier hal-00084629
Language en
contributor Laboratoire d'Informatique de Paris-Nord (LIPN) ; Université Paris 13 (UP13)-Institut Galilée-Université Sorbonne Paris Cité (USPC)-Centre National de la Recherche Scientifique (CNRS)
creator Baillot, Patrick
date 2005-05-10T00:00:00
harvest_object_id ea87c895-23cb-4130-996e-6af7d424fb54
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2024-11-29T00:00:00
set_spec type:COMM