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