Martín Abadi, Luca Cardelli, Pierre-Louis Curien & Jean-Jacques Lévy (1990):
Explicit Substitutions.
In: Frances E. Allen: Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, USA, January 1990.
ACM Press,
pp. 31–46,
doi:10.1145/96709.96712.
Beniamino Accattoli (2017):
(In)Efficiency and Reasonable Cost Models.
In: Sandra Alves & Renata Wasserman: 12th Workshop on Logical and Semantic Frameworks, with Applications, LSFA 2017, Brasília, Brazil, September 23-24, 2017,
Electronic Notes in Theoretical Computer Science 338.
Elsevier,
pp. 23–43,
doi:10.1016/j.entcs.2018.10.003.
Beniamino Accattoli & Ugo Dal Lago (2012):
On the Invariance of the Unitary Cost Model for Head Reduction.
In: Ashish Tiwari: 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan,
LIPIcs 15.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik,
pp. 22–37,
doi:10.4230/LIPIcs.RTA.2012.22.
Henk Barendregt, Wil Dekkers & Richard Statman (2013):
Lambda calculus with types.
Cambridge University Press,
doi:10.1017/CBO9781139032636.
Roel Bloo & Kristoffer H. Rose (1995):
Preservation of Strong Normalisation in Named Lambda Calculi with Explicit Substitution and Garbage Collection.
In: IN CSN-95: COMPUTER SCIENCE IN THE NETHERLANDS,
pp. 62–72.
Torben Braüner & Valeria De Paiva (1996):
Cut-elimination for full intuitionistic linear logic 10.
University of Cambridge, Computer Laboratory,
doi:10.7146/brics.v3i10.19973.
Gianluca Curzi & Luca Roversi (2020):
A type-assignment of linear erasure and duplication.
Theoretical Computer Science 837,
pp. 26–53,
doi:10.1016/j.tcs.2020.05.001.
Alejandro Díaz-Caro & Gilles Dowek (2013):
Non determinism through type isomorphism.
arXiv preprint arXiv:1303.7334.
Marco Gaboardi & Simona Ronchi Della Rocca (2009):
From light logics to type assignments: a case study.
Logic Journal of the IGPL 17(5),
pp. 499–530,
doi:10.1093/jigpal/jzp019.
Marco Gaboardi, Jean-Yves Marion & Simona Ronchi Della Rocca (2008):
Soft linear logic and polynomial complexity classes.
Electronic Notes in Theoretical Computer Science 205,
pp. 67–87,
doi:10.1016/j.entcs.2008.03.066.
Jean-Yves Girard (2017):
Proof-nets: the parallel syntax for proof-theory.
In: Logic and Algebra.
Routledge,
pp. 97–124,
doi:10.1201/9780203748671-4.
Jean-Yves Girard & Yves Lafont (1987):
Linear logic and lazy computation.
In: International Joint Conference on Theory and Practice of Software Development.
Springer,
pp. 52–66,
doi:10.1007/BFb0014972.
J Roger Hindley (1989):
BCK-combinators and linear λ-terms have types.
Theoretical Computer Science 64(1),
pp. 97–105,
doi:10.1016/0304-3975(89)90100-X.
Ross Horne (2019):
The sub-additives: A proof theory for probabilistic choice extending linear logic.
In: 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019).
Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,
doi:10.4230/LIPIcs.FSCD.2019.23.
Ugo Dal Lago & Simone Martini (2006):
An Invariant Cost Model for the Lambda Calculus.
In: Arnold Beckmann, Ulrich Berger, Benedikt Löwe & John V. Tucker: Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006, Proceedings,
Lecture Notes in Computer Science 3988.
Springer,
pp. 105–114,
doi:10.1007/11780342_11.
Harry G. Mairson (2004):
Linear Lambda Calculus and PTIME-completeness.
J. Funct. Program. 14(6),
pp. 623–633,
doi:10.1017/S0956796804005131.
Harry G. Mairson & Kazushige Terui (2003):
On the Computational Complexity of Cut-Elimination in Linear Logic.
In: Carlo Blundo & Cosimo Laneve: Theoretical Computer Science.
Springer Berlin Heidelberg,
Berlin, Heidelberg,
pp. 23–36,
doi:10.1007/978-3-540-45208-9_4.
Satoshi Matsuoka (2004):
Nondeterministic Linear Logic.
arXiv preprint cs/0410029.
François Maurel (2003):
Nondeterministic light logics and NP-time.
In: International Conference on Typed Lambda Calculi and Applications.
Springer,
pp. 241–255,
doi:10.1007/3-540-44904-3_17.
Paul-André Melliès (1995):
Typed Lambda-Calculi with Explicit Substitutions May Not Terminate.
In: Proceedings of the Second International Conference on Typed Lambda Calculi and Applications,
TLCA '95.
Springer-Verlag,
Berlin, Heidelberg,
pp. 328334,
doi:10.1007/BFb0014062.