Linear logic, type assignment systems and implicit computational complexity. (Logique linéaire, systèmes de types et complexité implicite)

Keywords

Descriptive complexity theory, Linear logic, Mathematics, Normalization (sociology), Lambda calculus

References

• To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and FormalismHaskell B. Curry, J. Roger Hindley, Jonathan P. Seldin — 1980
• Light Affine Calculus and Polytime Strong Normalization.Kazushige Terui — 2001
• Principal type-schemes and lambda-calculus semanticsMassimiliano Coppo, M. Dezani, Betti Venneri — 1980
• Foundations of software science and computational structures : 14th International Conference, FOSSACS 2011, held as part of the joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26 - April 3, 2011, proceedingsMartin Hofmann — 2011
• Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. ProceedingsC.-H. Luke Ong — 2011
• Review: Alan Cobham, Yehoshua Bar-Hillel, The Intrinsic Computational Difficulty of FunctionsS. Cook — 1969
• A Soft Type Assignment System for lambda -CalculusMarco Gaboardi, Simona Ronchi Della Rocca — 2007
• Lambda Calculus and Intuitionistic Linear LogicSimona Ronchi Della Rocca, Luca Roversi — 1997
• Linearity, Non-determinism and SolvabilityMichele Pagani, Simona Ronchi Della Rocca — 2010
• Calibrating computational feasibility by abstraction rankDaniël Leivant — 2002
• A type assignment for λ-calculus complete both for FPTIME and strong normalizationErika De Benedetti, Simona Ronchi Della Rocca — 2014
• Light Linear LogicJean-Yves Girard — 1994
• Bounded Linear Logic: A Modular Approach to Polynomial-Time ComputabilityJean-Yves Girard, Andre Scedrov, Philip Scott — 1992
• Light types for polynomial time computation in lambda-calculusPatrick Baillot, Kazushige Terui — 2004
• Quantum implicit computational complexityUgo Dal Lago, Andrea Masini, Margherita Zorzi — 2010
• Light Logics and the Call-by-Value Lambda CalculusPaolo Coppola, Ugo Dal Lago, Simona Ronchi Della Rocca — 2008
• A linearization of the Lambda-calculus and consequencesA. J. Kfoury — 1996
• Linear types and non-size-increasing polynomial time computationMartin Hofmann — 1999
• An elementary proof of strong normalization for intersection typesSilvio Valentini — 2001
• Church => Scott = Ptime: an application of resource sensitive realizabilityAloïs Brunel, Kazushige Terui — 2010

Cited by

• Strong Normalization through Intersection Types and MemoryAntonio Bucciarelli, Delia Kesner, Daniel Ventura — 2016
• Characterizing Polynomial and Exponential Complexity Classes in Elementary Lambda-CalculusPatrick Baillot, Erika De Benedetti, Simona Ronchi Della Rocca — 2014

Related papers

• Randomisation and Derandomisation in Descriptive Complexity TheoryKord Eickmeyer, Martin Grohe — 2010
• On the expressive power of monadic least fixed point logicNicole Schweikardt — 2006
• Characterizing time computational complexity classes with polynomial differential equationsRiccardo Gozzi, Daniel S. Graça — 2022
• On the expressivity of elementary linear logic: Characterizing Ptime and an exponential time hierarchyPatrick Baillot — 2015
• The complexity of first-order and monadic second-order logic revisitedMarkus Frick, Martin Grohe — 2004
• Structure in Complexity TheoryAlan L. Selman — 1986