@article(DBLP:journals/tcs/Accattoli15,
 author       = {Beniamino Accattoli},
 year         = {2015},
 title        = {Proof nets and the call-by-value {$\lambda$}-calculus},
 journal      = {Theor. Comput. Sci.},
 volume       = {606},
 pages        = {2--24},
 doi          = {10.1016/j.tcs.2015.08.006},
)
@inproceedings(DBLP:conf/lics/AccattoliC15,
 author       = {Beniamino Accattoli and Claudio Sacerdoti Coen},
 year         = {2015},
 title        = {On the Relative Usefulness of Fireballs},
 booktitle    = {30th Annual {ACM/IEEE} Symposium on Logic in Computer Science ({LICS} 2015)},
 publisher    = {{IEEE} Computer Society},
 pages        = {141--155},
 doi          = {10.1109/LICS.2015.23},
)
@article(DBLP:journals/pacmpl/AccattoliGK18,
 author       = {Beniamino Accattoli and Graham{-}Lengrand, St{\'{e}}phane and Delia Kesner},
 year         = {2018},
 title        = {Tight typings and split bounds},
 journal      = {{PACMPL}},
 volume       = {2},
 number       = {{ICFP}},
 pages        = {94:1--94:30},
 doi          = {10.1145/3236789},
)
@inproceedings(DBLP:conf/aplas/AccattoliG16,
 author       = {Beniamino Accattoli and Giulio Guerrieri},
 year         = {2016},
 title        = {Open Call-by-Value},
 editor       = {Atsushi Igarashi},
 booktitle    = {Programming Languages and Systems - 14th Asian Symposium ({APLAS} 2016)},
 series       = {Lecture Notes in Computer Science},
 volume       = {10017},
 publisher    = {Springer},
 pages        = {206--226},
 doi          = {10.1007/978-3-319-47958-3\_12},
)
@inproceedings(DBLP:conf/aplas/AccattoliG18,
 author       = {Beniamino Accattoli and Giulio Guerrieri},
 year         = {2018},
 title        = {Types of Fireballs},
 editor       = {Sukyoung Ryu},
 booktitle    = {Programming Languages and Systems - 16th Asian Symposium ({APLAS} 2018)},
 volume       = {11275},
 publisher    = {Springer},
 pages        = {45--66},
 doi          = {10.1007/978-3-030-02768-1\_3},
)
@inproceedings(DBLP:conf/esop/AccattoliGL19,
 author       = {Beniamino Accattoli and Giulio Guerrieri and Maico Leberle},
 year         = {2019},
 title        = {Types by Need},
 editor       = {Lu{\'{\i}}s Caires},
 booktitle    = {Programming Languages and Systems - 28th European Symposium on Programming ({ESOP} 2019)},
 series       = {Lecture Notes in Computer Science},
 volume       = {11423},
 publisher    = {Springer},
 pages        = {410--439},
 doi          = {10.1007/978-3-030-17184-1\_15},
)
@inproceedings(DBLP:conf/flops/AccattoliP12,
 author       = {Beniamino Accattoli and Luca Paolini},
 year         = {2012},
 title        = {Call-by-Value Solvability, Revisited},
 editor       = {Tom Schrijvers and Peter Thiemann},
 booktitle    = {Functional and Logic Programming - 11th International Symposium ({FLOPS} 2012)},
 series       = {Lecture Notes in Computer Science},
 volume       = {7294},
 publisher    = {Springer},
 pages        = {4--16},
 doi          = {10.1007/978-3-642-29822-6\_4},
)
@book(Barendregt84,
 author       = {Hendrik Pieter Barendregt},
 year         = {1984},
 title        = {The Lambda Calculus -- Its Syntax and Semantics},
 series       = {Studies in Logic and the Foundations of Mathematics},
 volume       = {103},
 publisher    = {North Holland},
 address      = {Amsterdam},
 doi          = {10.1016/B978-0-444-87508-2.50006-X},
)
@article(DBLP:journals/iandc/BenedettiR16,
 author       = {Erika De Benedetti and {Ronchi Della Rocca}, Simona},
 year         = {2016},
 title        = {A type assignment for {$\lambda$}-calculus complete both for {FPTIME} and strong normalization},
 journal      = {Inf. Comput.},
 volume       = {248},
 pages        = {195--214},
 doi          = {10.1016/j.ic.2015.12.012},
)
@article(DBLP:journals/corr/BernadetL13,
 author       = {Alexis Bernadet and St{\'{e}}phane Lengrand},
 year         = {2013},
 title        = {Non-idempotent intersection types and strong normalisation},
 journal      = {Logical Methods in Computer Science},
 volume       = {9},
 number       = {4},
 doi          = {10.2168/LMCS-9(4:3)2013},
)
@article(DBLP:journals/apal/BucciarelliE01,
 author       = {Antonio Bucciarelli and Thomas Ehrhard},
 year         = {2001},
 title        = {On phase semantics and denotational semantics: the exponentials},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {109},
 number       = {3},
 pages        = {205--241},
 doi          = {10.1016/S0168-0072(00)00056-7},
)
@article(DBLP:journals/apal/BucciarelliEM12,
 author       = {Antonio Bucciarelli and Thomas Ehrhard and Giulio Manzonetto},
 year         = {2012},
 title        = {A relational semantics for parallelism and non-determinism in a functional setting},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {163},
 number       = {7},
 pages        = {918--934},
 doi          = {10.1016/j.apal.2011.09.008},
)
@article(DBLP:journals/igpl/BucciarelliKV17,
 author       = {Antonio Bucciarelli and Delia Kesner and Daniel Ventura},
 year         = {2017},
 title        = {Non-idempotent intersection types for the Lambda-Calculus},
 journal      = {Logic Journal of the {IGPL}},
 volume       = {25},
 number       = {4},
 pages        = {431--464},
 doi          = {10.1093/jigpal/jzx018},
)
@inproceedings(DBLP:conf/fossacs/CarraroG14,
 author       = {Alberto Carraro and Giulio Guerrieri},
 year         = {2014},
 title        = {A Semantical and Operational Account of Call-by-Value Solvability},
 editor       = {Anca Muscholl},
 booktitle    = {Foundations of Software Science and Computation Structures - 17th International Conference ({FOSSACS} 2014)},
 series       = {Lecture Notes in Computer Science},
 volume       = {8412},
 publisher    = {Springer},
 pages        = {103--118},
 doi          = {10.1007/978-3-642-54830-7\_7},
)
@phdthesis(Carvalho07,
 author       = {Daniel de Carvalho},
 year         = {2007},
 title        = {S\'emantiques de la logique lin\'eaire et temps de calcul},
 type         = {{T}h\`ese de doctorat},
 school       = {Universit\'e Aix-Marseille II},
)
@article(deCarvalho18,
 author       = {Daniel de Carvalho},
 year         = {2018},
 title        = {Execution time of {$\lambda$}-terms via denotational semantics and intersection types},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {28},
 number       = {7},
 pages        = {1169--1203},
 doi          = {10.1017/S0960129516000396},
)
@article(DBLP:journals/tcs/CarvalhoPF11,
 author       = {Daniel de Carvalho and Michele Pagani and Lorenzo Tortora de Falco},
 year         = {2011},
 title        = {A semantic measure of the execution time in linear logic},
 journal      = {Theor. Comput. Sci.},
 volume       = {412},
 number       = {20},
 pages        = {1884--1902},
 doi          = {10.1016/j.tcs.2010.12.017},
)
@article(DBLP:journals/iandc/CarvalhoF16,
 author       = {Daniel de Carvalho and {Tortora de Falco}, Lorenzo},
 year         = {2016},
 title        = {A semantic account of strong normalization in linear logic},
 journal      = {Inf. Comput.},
 volume       = {248},
 pages        = {104--129},
 doi          = {10.1016/j.ic.2015.12.010},
)
@article(DBLP:journals/aml/CoppoD78,
 author       = {Mario Coppo and Dezani{-}Ciancaglini, Mariangiola},
 year         = {1978},
 title        = {A new type assignment for {$\lambda$}-terms},
 journal      = {Arch. Math. Log.},
 volume       = {19},
 number       = {1},
 pages        = {139--156},
 doi          = {10.1007/BF02011875},
)
@article(DBLP:journals/ndjfl/CoppoD80,
 author       = {Mario Coppo and Dezani{-}Ciancaglini, Mariangiola},
 year         = {1980},
 title        = {An extension of the basic functionality theory for the {$\lambda$}-calculus},
 journal      = {Notre Dame Journal of Formal Logic},
 volume       = {21},
 number       = {4},
 pages        = {685--693},
 doi          = {10.1305/ndjfl/1093883253},
)
@inproceedings(DBLP:conf/lfcs/Diaz-CaroMP13,
 author       = {D{\'{\i}}az{-}Caro, Alejandro and Giulio Manzonetto and Michele Pagani},
 year         = {2013},
 title        = {Call-by-Value Non-determinism in a Linear Logic Type Discipline},
 editor       = {Sergei N. Art{\"{e}}mov and Anil Nerode},
 booktitle    = {Logical Foundations of Computer Science, International Symposium ({LFCS} 2013)},
 series       = {Lecture Notes in Computer Science},
 volume       = {7734},
 publisher    = {Springer},
 pages        = {164--178},
 doi          = {10.1007/978-3-642-35722-0\_12},
)
@inproceedings(DBLP:conf/csl/Ehrhard12,
 author       = {Thomas Ehrhard},
 year         = {2012},
 title        = {Collapsing non-idempotent intersection types},
 editor       = {Patrick C{\'{e}}gielski and Arnaud Durand},
 booktitle    = {Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference},
 series       = {LIPIcs},
 volume       = {16},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
 pages        = {259--273},
 doi          = {10.4230/LIPIcs.CSL.2012.259},
)
@inproceedings(DBLP:conf/ppdp/EhrhardG16,
 author       = {Thomas Ehrhard and Giulio Guerrieri},
 year         = {2016},
 title        = {The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value},
 editor       = {James Cheney and Germ{\'{a}}n Vidal},
 booktitle    = {Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming ({PPDP} 2016)},
 publisher    = {{ACM}},
 pages        = {174--187},
 doi          = {10.1145/2967973.2968608},
)
@inproceedings(DBLP:conf/tacs/Gardner94,
 author       = {Philippa Gardner},
 year         = {1994},
 title        = {Discovering Needed Reductions Using Type Theory},
 booktitle    = {Theoretical Aspects of Computer Software ({TACS} '94)},
 series       = {Lecture Notes in Computer Science},
 volume       = {789},
 publisher    = {Springer},
 pages        = {555--574},
 doi          = {10.1007/3-540-57887-0_115},
)
@article(DBLP:journals/tcs/Girard87,
 author       = {Jean{-}Yves Girard},
 year         = {1987},
 title        = {Linear Logic},
 journal      = {Theor. Comput. Sci.},
 volume       = {50},
 pages        = {1--102},
 doi          = {10.1016/0304-3975(87)90045-4},
)
@article(DBLP:journals/apal/Girard88,
 author       = {Jean{-}Yves Girard},
 year         = {1988},
 title        = {Normal functors, power series and {$\lambda$}-calculus},
 journal      = {Ann. Pure Appl. Logic},
 volume       = {37},
 number       = {2},
 pages        = {129--177},
 doi          = {10.1016/0168-0072(88)90025-5},
)
@inproceedings(DBLP:conf/icfp/GregoireL02,
 author       = {Benjamin Gr{\'{e}}goire and Xavier Leroy},
 year         = {2002},
 title        = {A compiled implementation of strong reduction},
 editor       = {Mitchell Wand and {Peyton Jones}, Simon L.},
 booktitle    = {Proceedings of the Seventh International Conference on Functional Programming {(ICFP} '02)},
 publisher    = {{ACM}},
 pages        = {235--246},
 doi          = {10.1145/581478.581501},
)
@inproceedings(DBLP:conf/rta/Guerrieri15,
 author       = {Giulio Guerrieri},
 year         = {2015},
 title        = {Head reduction and normalization in a call-by-value lambda-calculus},
 editor       = {Yuki Chiba and Santiago Escobar and Naoki Nishida and David Sabel and Schmidt{-}Schau{\ss}, Manfred},
 booktitle    = {2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation ({WPTE} 2015)},
 series       = {{OASICS}},
 volume       = {46},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
 pages        = {3--17},
 doi          = {10.4230/OASIcs.WPTE.2015.3},
)
@article(Guerrieri18,
 author       = {Giulio Guerrieri},
 year         = {2018},
 title        = {Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (Long Version)},
 journal      = {CoRR},
 volume       = {abs/1812.10799},
 url          = {http://arxiv.org/abs/1812.10799},
)
@inproceedings(DBLP:conf/tlca/GuerrieriPR15,
 author       = {Giulio Guerrieri and Luca Paolini and Simona Ronchi Della Rocca},
 year         = {2015},
 title        = {Standardization of a Call-By-Value Lambda-Calculus},
 editor       = {Thorsten Altenkirch},
 booktitle    = {13th International Conference on Typed Lambda Calculi and Applications ({TLCA} 2015)},
 series       = {LIPIcs},
 volume       = {38},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
 pages        = {211--225},
 doi          = {10.4230/LIPIcs.TLCA.2015.211},
)
@article(DBLP:journals/lmcs/GuerrieriPR17,
 author       = {Giulio Guerrieri and Luca Paolini and Simona Ronchi Della Rocca},
 year         = {2017},
 title        = {Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus},
 journal      = {Logical Methods in Computer Science},
 volume       = {13},
 number       = {4},
 doi          = {10.23638/LMCS-13(4:29)2017},
)
@book(Jones:1993:PEA:153676,
 author       = {Neil D. Jones and Carsten K. Gomard and Peter Sestoft},
 year         = {1993},
 title        = {{Partial Evaluation and Automatic Program Generation}},
 publisher    = {Prentice-Hall, Inc.},
 address      = {Upper Saddle River, NJ, USA},
)
@inproceedings(DBLP:conf/ictac/KesnerV15,
 author       = {Delia Kesner and Daniel Ventura},
 year         = {2015},
 title        = {A Resource Aware Computational Interpretation for Herbelin's Syntax},
 editor       = {Martin Leucker and Camilo Rueda and Frank D. Valencia},
 booktitle    = {Theoretical Aspects of Computing - {ICTAC} 2015 - 12th International Colloquium},
 series       = {Lecture Notes in Computer Science},
 volume       = {9399},
 publisher    = {Springer},
 pages        = {388--403},
 doi          = {10.1007/978-3-319-25150-9\_23},
)
@inproceedings(DBLP:conf/rta/KesnerV17,
 author       = {Delia Kesner and Pierre Vial},
 year         = {2017},
 title        = {Types as Resources for Classical Natural Deduction},
 editor       = {Dale Miller},
 booktitle    = {2nd International Conference on Formal Structures for Computation and Deduction ({FSCD} 2017)},
 series       = {LIPIcs},
 volume       = {84},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
 pages        = {24:1--24:17},
 doi          = {10.4230/LIPIcs.FSCD.2017.24},
)
@article(DBLP:journals/logcom/Kfoury00,
 author       = {Assaf J. Kfoury},
 year         = {2000},
 title        = {A linearization of the Lambda-calculus and consequences},
 journal      = {J. Log. Comput.},
 volume       = {10},
 number       = {3},
 pages        = {411--436},
 doi          = {10.1093/logcom/10.3.411},
)
@book(DBLP:books/daglib/0071545,
 author       = {Jean{-}Louis Krivine},
 year         = {1993},
 title        = {Lambda-calculus, types and models},
 series       = {Ellis Horwood series},
 publisher    = {Ellis Horwood},
 address      = {Upper Saddle River, NJ, USA},
)
@article(DBLP:journals/pacmpl/MazzaPV18,
 author       = {Damiano Mazza and Luc Pellissier and Pierre Vial},
 year         = {2018},
 title        = {Polyadic approximations, fibrations and intersection types},
 journal      = {{PACMPL}},
 volume       = {2},
 number       = {{POPL}},
 pages        = {6:1--6:28},
 doi          = {10.1145/3158094},
)
@inproceedings(DBLP:conf/icfp/NeergaardM04,
 author       = {Peter M{\o}ller Neergaard and Harry G. Mairson},
 year         = {2004},
 title        = {Types, potency, and idempotency: why nonlinearity and amnesia make a type system work},
 editor       = {Chris Okasaki and Kathleen Fisher},
 booktitle    = {Proceedings of the Ninth International Conference on Functional Programming ({ICFP} 2004)},
 publisher    = {{ACM}},
 pages        = {138--149},
 doi          = {10.1145/1016850.1016871},
)
@inproceedings(DBLP:conf/ictcs/Paolini01,
 author       = {Luca Paolini},
 year         = {2001},
 title        = {Call-by-Value Separability and Computability},
 editor       = {Antonio Restivo and Simona Ronchi Della Rocca and Luca Roversi},
 booktitle    = {Theoretical Computer Science, 7th Italian Conference ({ICTCS} 2001)},
 series       = {Lecture Notes in Computer Science},
 volume       = {2202},
 publisher    = {Springer},
 pages        = {74--89},
 doi          = {10.1007/3-540-45446-2\_5},
)
@article(DBLP:journals/mscs/PaoliniPR17,
 author       = {Luca Paolini and Mauro Piccolo and {Ronchi Della Rocca}, Simona},
 year         = {2017},
 title        = {Essential and relational models},
 journal      = {Mathematical Structures in Computer Science},
 volume       = {27},
 number       = {5},
 pages        = {626--650},
 doi          = {10.1017/S0960129515000316},
)
@article(DBLP:journals/tcs/Plotkin75,
 author       = {Gordon D. Plotkin},
 year         = {1975},
 title        = {Call-by-Name, Call-by-Value and the lambda-Calculus},
 journal      = {Theor. Comput. Sci.},
 volume       = {1},
 number       = {2},
 pages        = {125--159},
 doi          = {10.1016/0304-3975(75)90017-1},
)
@inproceedings(Pottinger80,
 author       = {Garrel Pottinger},
 year         = {1980},
 title        = {A type assignment for the strongly normalizable $\lambda$-terms},
 editor       = {J.P. Seldin, J.R. Hindley},
 booktitle    = {To HB Curry: essays on combinatory logic, $\lambda$-calculus and formalism},
 publisher    = {Academic Press},
 pages        = {561--577},
)
@phdthesis(Reg:Thesis:92,
 author       = {Laurent Regnier},
 year         = {1992},
 title        = {{Lambda-calcul et r{\'e}seaux}},
 type         = {Ph{D} thesis},
 school       = {Univ. Paris VII},
)
@article(DBLP:journals/tcs/Regnier94,
 author       = {Laurent Regnier},
 year         = {1994},
 title        = {Une {\'{e}}quivalence sur les lambda-termes},
 journal      = {Theor. Comput. Sci.},
 volume       = {126},
 number       = {2},
 pages        = {281--292},
 doi          = {10.1016/0304-3975(94)90012-4},
)
@book(DBLP:series/txtcs/RoccaP04,
 author       = {{Ronchi Della Rocca}, Simona and Luca Paolini},
 year         = {2004},
 title        = {The Parametric Lambda Calculus - {A} Metamodel for Computation},
 series       = {Texts in Theoretical Computer Science. An {EATCS} Series},
 publisher    = {Springer},
 doi          = {10.1007/978-3-662-10394-4},
)