References

  1. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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.
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. 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.
  13. 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.
  14. 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.
  15. Daniel de Carvalho (2007): Sémantiques de la logique linéaire et temps de calcul. Thèse de doctorat. Université Aix-Marseille II.
  16. 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.
  17. 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.
  18. 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.
  19. Mario Coppo & Mariangiola Dezani-Ciancaglini (1978): A new type assignment for λ-terms. Arch. Math. Log. 19(1), pp. 139–156, doi:10.1007/BF02011875.
  20. 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.
  21. 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.
  22. 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.
  23. 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.
  24. 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.
  25. Jean-Yves Girard (1987): Linear Logic. Theor. Comput. Sci. 50, pp. 1–102, doi:10.1016/0304-3975(87)90045-4.
  26. 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.
  27. 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.
  28. 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.
  29. 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.
  30. 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.
  31. 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.
  32. Neil D. Jones, Carsten K. Gomard & Peter Sestoft (1993): Partial Evaluation and Automatic Program Generation. Prentice-Hall, Inc., Upper Saddle River, NJ, USA.
  33. 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.
  34. 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.
  35. 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.
  36. Jean-Louis Krivine (1993): Lambda-calculus, types and models. Ellis Horwood series. Ellis Horwood, Upper Saddle River, NJ, USA.
  37. 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.
  38. 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.
  39. 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.
  40. 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.
  41. 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.
  42. 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.
  43. Laurent Regnier (1992): Lambda-calcul et réseaux. PhD thesis. Univ. Paris VII.
  44. 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.
  45. 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.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org