Patrick Baillot

Title: Patrick Baillot

Research Question: How can we create a type system for lambda-calculus that ensures well-typed programs can be executed in polynomial time?

Methodology: The authors proposed a new type system called Dual Light Affine Logic (DLAL). It is a simplified version of Light Affine Logic (LAL), which is a logical system designed to characterize polynomial time computation. DLAL uses a linear and intuitionistic type arrow, and one modality. It corresponds to a fragment of Light Affine Logic.

Results: The authors showed that DLAL has good properties on lambda-terms. Subject reduction is satisfied, and a well-typed term admits a polynomial bound on reduction by any strategy. They also established that DLAL allows to represent all polynomial functions. Finally, they gave a type inference procedure for propositional DLAL.

Implications: DLAL offers several advantages over LAL. It has a smaller language of types, keeps the same properties as LAL, and ensures the complexity bound on the lambda-term itself. This means that the program part and the complexity specification are really separated. Additionally, DLAL type inference is conceptually easier, and it can be designed using a sub-procedure called Elementary Affine Logic (EAL) type inference. This has implications for the field of implicit computational complexity and programming languages.

Link to Article: https://arxiv.org/abs/0402059v1 Authors: arXiv ID: 0402059v1