A. Asperti & L. Roversi (2002):
Intuitionistic light affine logic.
ACM Transactions on Computational Logic 3(1),
pp. 1–39,
doi:10.1145/504077.504081.
P. Baillot & K. Terui (2009):
Light types for polynomial time computation in lambda-calculus.
Information and Computation 207(1),
pp. 41–62,
doi:10.1016/j.ic.2008.08.005.
Patrick Baillot & Kazushige Terui (2004):
Light types for polynomial time computation in lambda-calculus.
In: Proceedings of LICS'04,
pp. 266–275,
doi:10.1109/LICS.2004.1319621.
Stephen Bellantoni & Stephen A. Cook (1992):
A New Recursion-Theoretic Characterization of the Polytime Functions.
In: Proceedings of STOC'92.
ACM,
pp. 283–293.
A.K. Chandra, D.C. Kozen & L.J. Stockmeyer (1981):
Alternation.
Journal of the ACM 28(1),
pp. 114–133.
M. Gaboardi & S. Ronchi Della Ronca (2007):
A soft type assignment system for λ-calculus.
In: Proceedings of CSL'07.
Springer,
doi:10.1007/978-3-540-74915-8_21.
M. Gaboardi, S. Ronchi Della Ronca & J-Y Marion (2008):
A Logical Account of PSPACE.
In: Proceedings of POPL'08,
doi:10.1145/1328438.1328456.
J.-Y. Girard (1998):
Light Linear Logic.
Information and Computation 143,
pp. 175–204.
Martin Hofmann (2002):
The strength of non-size increasing computation.
In: Proceedings of POPL'02.
ACM,
pp. 260–269,
doi:10.1145/503272.503297.
J-L Krivine (2007):
A call-by-name lambda calculus machine.
Higher Order and Symbolic Computation.
Y. Lafont (2004):
Soft Linear Logic and polynomial time.
Theoretical Computer Science 318(1–2),
pp. 163–180,
doi:10.1016/j.tcs.2003.10.018.
Jean-Yves Marion & Daniel Leivant (1995):
Ramified Recurrence and Computational Complexity II: Substitution and Poly-Space.
In: Proceedings of CSL'94.
Springer,
pp. 486–500,
doi:10.1007/BFb0022277.
Jean-Yves Marion & Jean-Yves Moyen (2000):
Efficient First Order Functional Program Interpreter with Time Bound Certifications.
In: Proceedings of LPAR'00.
Springer,
pp. 25–42,
doi:10.1007/3-540-44404-1_3.
eptcs@eptcs.org