Light logics and optimal reduction: Completeness and complexity

Girard, 1998, Light linear logic, Information and Computation, 143, 175, 10.1006/inco.1998.2700 Asperti, 1998, Light affine logic, 300 Asperti, 2002, Intuitionistic light affine logic, ACM Transactions on Computational Logic, 3, 1, 10.1145/504077.504081 Coppola, 2006, Optimizing optimal reduction. A type inference algorithm for elementary affine logic, ACM Transactions on Computational Logic, 7, 219, 10.1145/1131313.1131315 Coppola, 2005, Principal typing for lambda calculus in elementary affine logic, Fundamenta Informaticae, 65, 87 Atassi, 2007, Verification of P time reducibility for system F terms: type inference in dual light affine logic, Logical Methods in Computer Science, 3, 1 Baillot, 2009, Light types for polynomial time computation in lambda calculus, Information and Computation, 207, 41, 10.1016/j.ic.2008.08.005 P. Coppola, U. Dal Lago, S. Ronchi Della Rocca, Elementary affine logic and the call-by-value lambda calculus, in: Proceedigs of TLCA 2005, LNCS, vol. 3461, Springer, 2005, pp. 131–145. Laurent, 2006, Obsessional cliques: a semantic characterization of bounded time complexity, 179 A.S. Murawski, C.-H.L. Ong, Discreet games, light affine logic and PTIME computation, in: Proceedings of CSL 2000, LNCS, vol. 1862, Springer, 2000, pp. 427–441. U. Dal Lago, M. Hofmann, Quantitative models and implicit complexity, in: Proceedings of FSTTCS 2005, LNCS, vol. 3821, Springer, 2005, pp. 189–200. Lamping, 1990, An algorithm for optimal lambda calculus reduction, 16 Pedicini, 2000, A parallel implementation for optimal lambda-calculus reduction, 3 Lawall, 1996, Optimality and inefficiency: what isn’t a cost model of the lambda calculus?, 92 Asperti, 2001, Parallel beta reduction is not elementary recursive, Information and Computation, 170, 49, 10.1006/inco.2001.2869 Asperti, 2004, (Optimal) duplication is not elementary recursive, Information and Computation, 193, 21, 10.1016/j.ic.2004.05.001 Asperti, 1998 Gonthier, 1992, The geometry of optimal lambda reduction, 15 J.-Y. Girard, Geometry of interaction 1: interpretation of system F, in: Proceedings Logic Colloquium 1988, 1989, pp. 221–260. Danos, 1995, Proof-nets and the Hilbert space, 307 Danos, 1999, Reversible, irreversible and optimal lambda-machines, Theoretical Computer Science, 227, 79, 10.1016/S0304-3975(99)00049-3 Dal Lago, 2006, Context semantics, linear logic and computational complexity, 169 A. Asperti, V. Danos, C. Laneve, L. Regnier, Paths in the lambda-calculus, in: Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science (LICS’94), IEEE Computer Society, 1994, pp. 426–436. V. Danos, La logique Linéaire appliquée à l’étude de divers processus de normalisation (principalement du λ-calcul), Ph.D. thesis, Université Paris VII, 1990. L. Regnier, Lambda-Calcul et réseaux, Ph.D. thesis, Université Paris VII, 1992. H. Mairson, From Hilbert spaces to Dilbert spaces: context semantics made simple, in: Proceedings of FSTTCS 2002, LNCS, vol. 2556, 2002, pp. 2–17. Guerrini, 1999, A general theory of sharing graphs, Theoretical Computer Science, 227, 99, 10.1016/S0304-3975(99)00050-X Guerrini, 2003, Coherence for sharing proof-nets, Theoretical Computer Science, 294, 379, 10.1016/S0304-3975(01)00162-1 Lafont, 1997, Interaction combinators, Information and Computation, 137, 69, 10.1006/inco.1997.2643 Dal Lago, 2006, Light affine logic, uniform encodings and polynomial time, Mathematical Structures in Computer Science, 16, 713, 10.1017/S0960129506005421 P. Baillot, K. Terui, A feasible algorithm for typing in elementary affine logic, in: Proceedings of TLCA 2005, LNCS, vol. 3461, Springer, 2005, pp. 55–70. Danos, 1989, The structure of multiplicatives, Archive for Mathematical Logic, 28, 181, 10.1007/BF01622878 Baillot, 2001, Elementary complexity and geometry of interaction, Fundamenta Informaticae, 45, 1 V. Atassi, Typing and optimal reduction for lambda calculus in variants of linear logic for implicit computational complexity, Ph.D. thesis, Université Paris 13, 2008.