[. Accattoli, E. Bonelli, D. Kesner, and C. Lombardi, A nonstandard standardization theorem, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pp.659-670, 2014.
DOI : 10.1145/2535838.2535886

B. Accattoli, P. Barenbaum, and D. Mazza, Distilling abstract machines, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pp.363-376, 2014.

B. Accattoli, An abstract factorization theorem for explicit substitutions On the invariance of the unitary cost model for head reduction, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012 B. ACCATTOLI AND U. DAL LAGO [ADL14a, pp.6-21, 2012.

B. Accattoli and U. D. Lago, Beta reduction is invariant, indeed, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, p.8, 2014.
DOI : 10.1145/2603088.2603105
URL : https://hal.archives-ouvertes.fr/hal-01091551

B. Accattoli and U. D. Lago, Beta reduction is invariant, indeed (long version) Technical report associated to [ADL14a], Available at http://arxiv.org/abs/1405, AG09] Beniamino Accattoli and Stefano Guerrini. Jumping boxes. In Computer Science Logic 18th Annual Conference of the EACSL. Proceedings, pp.55-70, 2009.

A. Asperti and H. G. Mairson, Parallel beta reduction is not elementary recursive, POPL '98, Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.303-315, 1998.

M. Avanzini, G. Accattoli, and C. Sacerdoti-coen, On the value of variables, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010 Logic, Language , Information, and Computation -21st International Workshop, WoLLIC 2014ASC15] Beniamino Accattoli and Claudio Sacerdoti Coen. On the relative usefulness of fireballs 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, pp.33-48, 2010.

H. P. Barendregt, The Lambda Calculus ? Its Syntax and Semantics, 1984.

E. Guy, J. Blelloch, and . Greiner, Parallelism in sequential functional languages, FPCA, pp.226-237, 1995.

A. Bernadet and S. Lengrand, Non-idempotent intersection types and strong normalisation, Logical Methods in Computer Science, vol.9, issue.4, p.2013
DOI : 10.2168/LMCS-9(4:3)2013
URL : https://hal.archives-ouvertes.fr/hal-00906778

P. Baillot, K. Terui-nicolaas, and G. De-bruijn, Light types for polynomial time computation in lambda calculus, Mathematical Logic and Theoretical Computer Science, number 106 in Lecture Notes in Pure and Applied Mathematics, pp.41-62, 1987.
DOI : 10.1016/j.ic.2008.08.005
URL : https://hal.archives-ouvertes.fr/hal-00012752

C. Daniel-de, M. Daniel-de-carvalho, L. Pagani, and . Tortora-de-falco, Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905 A semantic measure of the execution time in linear logic, Theor. Comput. Sci, vol.4251, issue.20, pp.4121884-1902, 2009.

P. Coppola, U. D. Lago, and S. Rocca, Light logics and the call-byvalue lambda calculus, CF58] H.B. Curry and R. Feys. Combinatory Logic. Studies in logic and the foundations of mathematics, 1958.

P. Clairambault, Bounding Skeletons, Locally Scoped Terms and Exact Bounds for Linear Head Reduction, Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013 Proceedings, pp.109-124, 2013.
DOI : 10.1007/978-3-642-38946-7_10

U. Dal, L. , and O. Laurent, Quantitative game semantics for linear logic, Computer Science Logic 17th Annual Conference of the EACSL Proceedings, pp.230-245, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00270933

U. Dal, L. , and S. Martini, The weak lambda calculus as a reasonable machine, Theor. Comput. Sci, vol.398, issue.1-3, pp.32-50, 2008.

U. Dal, L. , and S. Martini, On constructor rewrite systems and the lambda calculus, Logical Methods in Computer Science, vol.8, issue.3, p.2012

U. Dal, L. , and U. Schöpp, Functional programming in sublinear space Held as Part of the Joint European Conferences on Theory and Practice of Software, Programming Languages and Systems, 19th European Symposium on Programming Proceedings, pp.205-225, 2010.

V. Danos and L. Regnier, Head linear reduction [FS91] Gudmund Skovbjerg Frandsen and Carl Sturtivant What is an efficient implementation of the ?-calculus? In Functional Programming Languages and Computer Architecture, 5th ACM Conference Proceedings, pp.289-312, 1991.

D. R. Ghica, Slot games: a quantitative model of computation, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, pp.85-97, 2005.

B. Grégoire and X. Leroy, A compiled implementation of strong reduction, Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02)GLM92] Georges Gonthier, Jean-Jacques Lévy, and Paul-AndréMellì es. An abstract standardisation theorem Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), pp.235-246, 1992.

M. Gaboardi, J. Marion, and S. Rocca, A logical account of pspace, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.121-131, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00342323

M. Gaboardi and S. Rochel, A soft type assignment system for lambda -calculus Maximal sharing in the lambda calculus with letrec, Computer Science Logic, 21st International Workshop 16th Annual Conference of the EACSL Proceedings Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, pp.253-267, 2007.

N. D. Jones, What not to do when writing an interpreter for specialisation, In Partial Evaluation, International Seminar, pp.216-237, 1996.
DOI : 10.1007/3-540-61580-6_11

J. Lévy, Réductions correctes et optimales dans le lambda-calcul, Thése d'Etat, 1978.

J. L. Lawall and H. G. Mairson, Optimality and inefficiency: What isn't a cost model of the lambda calculus, Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (ICFP '96), pp.92-101, 1996.

J. Laird, G. Manzonetto, G. Mccusker, and M. Pagani, Weighted Relational Models of Typed Lambda-Calculi, 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pp.301-310, 2013.
DOI : 10.1109/LICS.2013.36
URL : https://hal.archives-ouvertes.fr/hal-01144064

D. Mazza, Simple parsimonious types and logarithmic space, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015, pp.24-40, 2015.

P. Es, Description Abstraite de système de réécriture, 1996.

R. Milner, Local Bigraphs and Confluence: Two Conjectures, Electronic Notes in Theoretical Computer Science, vol.175, issue.3, pp.65-73, 1992.
DOI : 10.1016/j.entcs.2006.07.035

J. Simon-peyton, The Implementation of Functional Programming Languages. International Series in Computer Science, 1987.

U. Schöpp, Stratified bounded affine logic for logarithmic space Lambda calculi and linear speedups, 22nd IEEE Symposium on Logic in Computer Science The Essence of Computation 46 B. ACCATTOLI AND U. DAL LAGO [SR15], pp.10-12, 2002.

G. Scherer and D. Rémy, Full Reduction in the Face of Absurdity, Programming Languages and Systems -24th European Symposium on Programming, ESOP 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software Proceedings, pp.685-709, 2015.
DOI : 10.1007/978-3-662-46669-8_28
URL : https://hal.archives-ouvertes.fr/hal-01093910

R. Statman, The typed ??-calculus is not elementary recursive, Theoretical Computer Science, vol.9, issue.1, pp.73-81, 1979.
DOI : 10.1016/0304-3975(79)90007-0

F. Cees, P. Slot, . Van-emde, and . Boas, On tape versus core; an application of space efficient perfect hash functions to the invariance of space, Proceedings of the 16th Annual ACM Symposium on Theory of ComputingWad71] C. P. Wadsworth. Semantics and pragmatics of the lambda-calculus, pp.391-400, 1971.