pith. sign in

arxiv: 2402.12078 · v4 · submitted 2024-02-19 · 💻 cs.LO

Mirroring Call-by-Need, or Values Acting Silly

Beniamino Accattoli , Adrienne Lancelot This is my paper

Pith reviewed 2026-05-24 04:05 UTC · model grok-4.3

classification 💻 cs.LO
keywords lambda calculuscall-by-needcall-by-valuecontextual equivalenceevaluation strategiesmulti typesrewritingabstract machines
0
0 comments X

The pith

Call-by-silly merges the worst traits of call-by-name and call-by-value yet produces exactly the same contextual equivalence as call-by-value.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper designs call-by-silly as a degenerate calculus that pairs the wasteful duplications of call-by-name with the wasteful erasures of call-by-value. It proves that this calculus and ordinary call-by-value define identical contextual equivalences on lambda terms. The result mirrors the known fact that call-by-need and call-by-name are contextually equivalent, thereby exposing how call-by-value equivalence remains blind to efficiency. The argument rests on rewriting properties, multi-type characterizations, a concrete strategy, and an abstract machine that implements maximal-length sequences.

Core claim

Call-by-silly merges the worst behaviors of call-by-name and call-by-value. The main theorem states that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. The design is validated via rewriting properties and multi types; a call-by-silly strategy is defined, implemented by an abstract machine, measured by tight multi types, and shown to compute evaluation sequences of maximal length.

What carries the argument

The call-by-silly calculus obtained by merging silly duplications from call-by-name with silly erasures from call-by-value, together with its multi-type system and maximal-length strategy.

If this is right

  • Call-by-value contextual equivalence cannot distinguish programs that differ only in the number of duplications or erasures performed.
  • The call-by-silly strategy always yields the longest possible reduction sequences inside the calculus.
  • Tight multi types give exact upper and lower bounds on the length of call-by-silly computations.
  • The abstract machine implements the call-by-silly strategy without adding or omitting steps.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Similar worst-case degenerations could be constructed for other pairs of strategies to test the coarseness of their equivalences.
  • Contextual equivalence may need to be replaced by cost-sensitive relations when efficiency distinctions matter in language design.
  • The multi-type technique used here could be adapted to bound costs in calculi that mix duplication and erasure differently.

Load-bearing premise

The particular merging of worst-case behaviors that defines call-by-silly still yields a calculus whose contextual equivalence with call-by-value can be proved without extra restrictions.

What would settle it

Two terms that are contextually equivalent under call-by-value but separated by a call-by-silly context, or the converse.

Figures

Figures reproduced from arXiv: 2402.12078 by Adrienne Lancelot, Beniamino Accattoli.

Figure 1
Figure 1. Figure 1: Variants of the linear substitution calculus (LSC). [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The silly multi type system. Lemma 4.7 (Strict strong local commutations). Reduction →we (resp. →we; resp. →wgcv) strictly strongly commutes over →wm (resp. →wgcv; resp. →wm). Proof. The three points are all proved by unsurprising inductions on one of the spanning steps and case analysis of the other spanning step. All the details can be found in [AL24]. Theorem 4.8 (Confluence). Reductions →w and →w¬gcv a… view at source ↗
Figure 3
Figure 3. Figure 3: The call-by-value λ-calculus. • C = λx.C′ : all derivations of C⟨t⟩ and C⟨u⟩ must start with the typing rule axλ or the typing rule λ. For axλ, it is trivial to conclude. For λ, it follows from the i.h. on the premise of the rule. • C = C ′ s: all derivations of C⟨t⟩ and C⟨u⟩ must start with the typing rule @. It follows from the i.h. on the left premise of the rule @. • Other cases follow the same argumen… view at source ↗
Figure 4
Figure 4. Figure 4: The call-by-name strategy. A state is final if no transitions apply. A run r : Q ⇝∗ Q ′ is a possibly empty finite sequence of transitions, the length of which is noted |r|; note that the first and the last states of a run are not necessarily initial and final. If a and b are transitions labels (that is, ⇝a⊆⇝ and ⇝b⊆⇝) then ⇝a,b:=⇝a ∪ ⇝b and |r|a is the number of a transitions in r, |r|a,b := |r|a +|r|b, a… view at source ↗
Figure 5
Figure 5. Figure 5: The Milner Abstract Machine (MAM). The MAM. The MAM is an abstract machine for the CbN strategy, defined in [PITH_FULL_IMAGE:figures/full_fig_p025_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Structural reduction for simulating the MAM. [PITH_FULL_IMAGE:figures/full_fig_p026_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: The Silly Milner Abstract Machine (Silly MAM). [PITH_FULL_IMAGE:figures/full_fig_p028_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Structural reductions. Structural Reductions. As for the MAM, the simulation of transition m requires the structural reduction ⇛@l . The presence of the partial answer data structure A, however, forces us to introduce a further structural reduction ⇛ans. It is defined in [PITH_FULL_IMAGE:figures/full_fig_p030_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: The call-by-silly strategy →y. search transparency (Prop. 10.8.2) applied to r ′′, one obtains a one-step evaluation f : Q ′ →a⇛ Q ′′ = Q. Concatenating e and f, we obtain an evaluation g : t →∗ w¬gcv⇛ Q ′ →w¬gcv⇛ Q. Postponing structural reduction (Prop. 10.7), we obtain the required evaluation d: t →∗ w¬gcv⇛ Q. (2) Cases of |d| ∈ N: • |d| = 0. Then t = a. Since decoding is the inverse of initialization, … view at source ↗
read the original abstract

Call-by-need evaluation for the lambda-calculus can be seen as merging the best of call-by-name and call-by-value, namely the wise erasing behaviour of the former and the wise duplicating behaviour of the latter. To better understand how duplication and erasure can be combined, we design a degenerated calculus, dubbed call-by-silly, that is symmetric to call-by-need in that it merges the worst of call-by-name and call-by-value, namely silly duplications by-name and silly erasures by-value. We validate the design of the call-by-silly calculus via rewriting properties and multi types. In particular, we mirror the main theorem about call-by-need -- that is, its operational equivalence with call-by-name -- showing that call-by-silly and call-by-value induce the same contextual equivalence. This fact shows the blindness with respect to efficiency of call-by-value contextual equivalence. We also define a call-by-silly strategy and a call-by-silly abstract machine implementing the strategy. Moreover, we measure the number of steps taken by the strategy via tight multi types. Lastly, we prove that the call-by-silly strategy computes evaluation sequences of maximal length in the calculus.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript introduces the call-by-silly calculus, obtained by merging the worst-case duplication behavior of call-by-name with the worst-case erasure behavior of call-by-value. It validates the design via rewriting properties and multi-type characterizations, then proves that call-by-silly and call-by-value induce identical contextual equivalences (mirroring the known call-by-need / call-by-name result). Further contributions include a call-by-silly reduction strategy, an abstract machine implementing it, tight multi-type bounds on the number of steps, and a proof that the strategy realizes evaluation sequences of maximal length.

Significance. If the central equivalence theorem holds, the work supplies a symmetric counterpart to call-by-need that clarifies the roles of duplication and erasure; the result that call-by-value contextual equivalence cannot distinguish efficiency differences is a useful negative observation for the study of observational equivalences. The combination of rewriting analysis, multi types for both equivalence and complexity, and an abstract machine is a coherent methodological package.

minor comments (3)
  1. [§3] §3 (or the section defining the call-by-silly rules): the reduction rules should be presented in a side-by-side table with the corresponding call-by-name and call-by-value rules to make the 'worst of both' construction immediately visible.
  2. The multi-type system used for the contextual-equivalence proof and the one used for tight step bounds appear to be the same; if they differ, the distinction should be stated explicitly when the equivalence theorem is proved.
  3. The abstract machine section would benefit from a short diagram or pseudocode excerpt showing the key transition rules that implement the silly duplication and erasure behaviors.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, significance assessment, and recommendation of minor revision. No specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines call-by-silly by merging worst-case behaviors from CBN and CBV, then validates the design and proves contextual equivalence to CBV via independent rewriting properties and multi-type characterizations (mirroring but not depending on the CBN/CBN-need result). No derivation step reduces by construction to fitted inputs, self-definitions, or load-bearing self-citations; the equivalence follows from the stated techniques without circular reduction.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper relies on standard lambda-calculus axioms for rewriting and typing; it introduces the call-by-silly calculus as a new construction without independent evidence beyond the paper's own definitions and proofs.

axioms (1)
  • standard math Standard lambda-calculus reduction rules and contextual equivalence definitions
    Invoked throughout for defining call-by-silly behavior and equivalence.
invented entities (1)
  • call-by-silly calculus no independent evidence
    purpose: Degenerate symmetric counterpart to call-by-need that merges worst-case duplication and erasure
    Newly defined in the paper; no external falsifiable evidence provided.

pith-pipeline@v0.9.0 · 5739 in / 1221 out tokens · 21582 ms · 2026-05-24T04:05:44.457342+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

57 extracted references · 57 canonical work pages · 1 internal anchor

  1. [1]

    Environments and the complexity of abstract machines

    Beniamino Accattoli and Bruno Barras. Environments and the complexity of abstract machines. In Proceedings of the 19th International Symposium on Principles and Practice of Declarative Programming ( PPDP 2017) , pages 4--16, 2017. URL: http://doi.acm.org/10.1145/3131851.3131855

    work page doi:10.1145/3131851.3131855 2017

  2. [2]

    The negligible and yet subtle cost of pattern matching

    Beniamino Accattoli and Bruno Barras. The negligible and yet subtle cost of pattern matching. In Bor - Yuh Evan Chang, editor, Programming Languages and Systems - 15th Asian Symposium, APLAS 2017, Suzhou, China, November 27-29, 2017, Proceedings , volume 10695 of Lecture Notes in Computer Science , pages 426--447. Springer, 2017. https://doi.org/10.1007/9...

    work page doi:10.1007/978-3-319-71237-6 2017

  3. [3]

    A nonstandard standardization theorem

    Beniamino Accattoli, Eduardo Bonelli, Delia Kesner, and Carlos Lombardi. A nonstandard standardization theorem. In Suresh Jagannathan and Peter Sewell, editors, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014 , pages 659--670. ACM , 2014. https://doi.org/10.1145/2535838...

    work page doi:10.1145/2535838.2535886 2014

  4. [4]

    Distilling abstract machines

    Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. Distilling abstract machines. In Johan Jeuring and Manuel M. T. Chakravarty, editors, Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1-3, 2014 , pages 363--376. ACM , 2014. https://doi.org/10.1145/2628136.2628154 doi:10.1145/2628...

    work page doi:10.1145/2628136.2628154 2014

  5. [5]

    A strong distillery

    Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. A strong distillery. In Xinyu Feng and Sungwoo Park, editors, Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings , volume 9458 of Lecture Notes in Computer Science , pages 231--250. Springer, 2015. https://doi.org/10...

    work page doi:10.1007/978-3-319-26529-2 2015

  6. [6]

    An abstract factorization theorem for explicit substitutions

    Beniamino Accattoli. An abstract factorization theorem for explicit substitutions. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA'12) , RTA 2012, May 28 - June 2, 2012, Nagoya, Japan , volume 15 of LIPIcs , pages 6--21. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2012. https://doi.org/10.4...

    work page doi:10.4230/lipics.rta.2012.6 2012

  7. [7]

    Proof nets and the call-by-value \( \) -calculus

    Beniamino Accattoli. Proof nets and the call-by-value \( \) -calculus. Theor. Comput. Sci. , 606:2--24, 2015. https://doi.org/10.1016/j.tcs.2015.08.006 doi:10.1016/j.tcs.2015.08.006

    work page doi:10.1016/j.tcs.2015.08.006 2015

  8. [8]

    Proof nets and the linear substitution calculus

    Beniamino Accattoli. Proof nets and the linear substitution calculus. In Bernd Fischer and Tarmo Uustalu, editors, Theoretical Aspects of Computing - ICTAC 2018 - 15th International Colloquium, Stellenbosch, South Africa, October 16-19, 2018, Proceedings , volume 11187 of Lecture Notes in Computer Science , pages 37--61. Springer, 2018. https://doi.org/10...

    work page doi:10.1007/978-3-030-02508-3 2018

  9. [9]

    Exponentials as substitutions and the cost of cut elimination in linear logic

    Beniamino Accattoli. Exponentials as substitutions and the cost of cut elimination in linear logic. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022 , pages 49:1--49:15. ACM , 2022. https://doi.org/10.1145/3531130.3532445 doi:10.1145/3531130.3532445

    work page doi:10.1145/3531130.3532445 2022

  10. [10]

    Exponentials as substitutions and the cost of cut elimination in linear logic

    Beniamino Accattoli. Exponentials as substitutions and the cost of cut elimination in linear logic. Log. Methods Comput. Sci. , 19(4), 2023. https://doi.org/10.46298/LMCS-19(4:23)2023 doi:10.46298/LMCS-19(4:23)2023

    work page doi:10.46298/lmcs-19(4:23)2023 2023

  11. [11]

    Lineal: A linear-algebraic lambda-calculus

    Pablo Arrighi and Gilles Dowek. Lineal: A linear-algebraic lambda-calculus. Log. Methods Comput. Sci. , 13(1), 2017. https://doi.org/10.23638/LMCS-13(1:8)2017 doi:10.23638/LMCS-13(1:8)2017

    work page doi:10.23638/lmcs-13(1:8)2017 2017

  12. [13]

    Ariola, Matthias Felleisen, John Maraist, Martin Oder- sky, and Philip Wadler

    Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. In Ron K. Cytron and Peter Lee, editors, Conference Record of POPL'95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995 , pages 233--246. ACM Press, 1995. https:...

    work page doi:10.1145/199448.199507 1995

  13. [14]

    Open call-by-value

    Beniamino Accattoli and Giulio Guerrieri. Open call-by-value. In Atsushi Igarashi, editor, Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings , volume 10017 of Lecture Notes in Computer Science , pages 206--226, 2016. https://doi.org/10.1007/978-3-319-47958-3\_12 doi:10.1007/978-3-319-47...

    work page doi:10.1007/978-3-319-47958-3 2016

  14. [15]

    The theory of call-by-value solvability

    Beniamino Accattoli and Giulio Guerrieri. The theory of call-by-value solvability. Proc. ACM Program. Lang. , 6( ICFP ):855--885, 2022. https://doi.org/10.1145/3547652 doi:10.1145/3547652

    work page doi:10.1145/3547652 2022

  15. [16]

    Tight typings and split bounds, fully developed

    Beniamino Accattoli, St \' e phane Graham - Lengrand, and Delia Kesner. Tight typings and split bounds, fully developed. J. Funct. Program. , 30:e14, 2020. https://doi.org/10.1017/S095679682000012X doi:10.1017/S095679682000012X

    work page doi:10.1017/s095679682000012x 2020

  16. [17]

    Types by need

    Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Types by need. In Proceedings of the 28th European Symposium on Programming ( ESOP 2019) , pages 410--439, 2019. https://doi.org/10.1007/978-3-030-17184-1\_15 doi:10.1007/978-3-030-17184-1\_15

    work page doi:10.1007/978-3-030-17184-1 2019

  17. [18]

    Ariola, Hugo Herbelin, and Alexis Saurin

    Zena M. Ariola, Hugo Herbelin, and Alexis Saurin. Classical call-by-need and duality. In C. - H. Luke Ong, editor, Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings , volume 6690 of Lecture Notes in Computer Science , pages 27--44. Springer, 2011. https://doi.org/10.1007/978-3-6...

    work page doi:10.1007/978-3-642-21691-6 2011

  18. [19]

    The structural lambda-calculus

    Beniamino Accattoli and Delia Kesner. The structural lambda-calculus. In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. Proceedings , volume 6247 of Lecture Notes in Computer Science , pages 381--395. Springer, 2010. https:/...

    work page doi:10.1007/978-3-642-15205-4 2010

  19. [20]

    o ttingen, Germany (Virtual Conference) , volume 216 of LIPIcs , pages 4:1--4:21. Schloss Dagstuhl - Leibniz-Zentrum f \

    Beniamino Accattoli and Maico Leberle. Useful open call-by-need. In Florin Manea and Alex Simpson, editors, 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, February 14-19, 2022, G \" o ttingen, Germany (Virtual Conference) , volume 216 of LIPIcs , pages 4:1--4:21. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Informatik, 2022. https://doi....

    work page doi:10.4230/lipics.csl.2022.4 2022

  20. [21]

    Mirroring Call-by-Need, or Values Acting Silly

    Beniamino Accattoli and Adrienne Lancelot. Mirroring call-by-need, or values acting silly (v2), 2024. https://arxiv.org/abs/2402.12078v2 arXiv:2402.12078v2

    work page internal anchor Pith review Pith/arXiv arXiv 2024

  21. [22]

    The cost of skeletal call-by-need, smoothly

    Beniamino Accattoli, Francesco Magliocca, Lo \" c Peyrot, and Claudio Sacerdoti Coen. The cost of skeletal call-by-need, smoothly. In Maribel Fern \' a ndez, editor, 10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025, July 14-20, 2025, Birmingham, UK , volume 337 of LIPIcs , pages 5:1--5:22. Schloss Dagstuhl - Leib...

    work page doi:10.4230/lipics.fscd.2025.5 2025

  22. [23]

    Call-by-value solvability, revisited

    Beniamino Accattoli and Luca Paolini. Call-by-value solvability, revisited. In Tom Schrijvers and Peter Thiemann, editors, Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings , volume 7294 of Lecture Notes in Computer Science , pages 4--16. Springer, 2012. https://doi.org/10.1007/978-3-642...

    work page doi:10.1007/978-3-642-29822-6 2012

  23. [24]

    On the R elative U sefulness of F ireballs

    Beniamino Accattoli and Claudio Sacerdoti Coen. On the R elative U sefulness of F ireballs. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015 , pages 141--155. IEEE Computer Society, 2015. https://doi.org/10.1109/LICS.2015.23 doi:10.1109/LICS.2015.23

    work page doi:10.1109/lics.2015.23 2015

  24. [25]

    Foundations of strong call by need

    Thibaut Balabonski, Pablo Barenbaum, Eduardo Bonelli, and Delia Kesner. Foundations of strong call by need. PACMPL , 1( ICFP ):20:1--20:29, 2017. https://doi.org/10.1145/3110264 doi:10.1145/3110264

    work page doi:10.1145/3110264 2017

  25. [26]

    Pattern matching and fixed points: Resource types and strong call-by-need: Extended abstract

    Pablo Barenbaum, Eduardo Bonelli, and Kareem Mohamed. Pattern matching and fixed points: Resource types and strong call-by-need: Extended abstract. In David Sabel and Peter Thiemann, editors, Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018 ,...

    work page doi:10.1145/3236950.3236972 2018

  26. [27]

    Solvability = typability + inhabitation

    Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. Solvability = typability + inhabitation. Log. Methods Comput. Sci. , 17(1), 2021. URL: https://lmcs.episciences.org/7141

    work page 2021

  27. [28]

    Complexity of strongly normalising \( \) -terms via non-idempotent intersection types

    Alexis Bernadet and St \' e phane Lengrand. Complexity of strongly normalising \( \) -terms via non-idempotent intersection types. In FOSSACS 2011 , pages 88--107, 2011. https://doi.org/10.1007/978-3-642-19805-2_7 doi:10.1007/978-3-642-19805-2_7

    work page doi:10.1007/978-3-642-19805-2_7 2011

  28. [29]

    A strong call-by-need calculus

    Thibaut Balabonski, Antoine Lanco, and Guillaume Melquiond. A strong call-by-need calculus. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference) , volume 195 of LIPIcs , pages 9:1--9:22. Schloss Dagstuhl - Leibniz-Zentrum f \" ...

    work page doi:10.4230/lipics.fscd.2021.9 2021

  29. [30]

    URL https://doi.org/10.1007/978-3-030-17127-8_ 13

    Dariusz Biernacki, Sergue \" Lenglet, and Piotr Polesiuk. A complete normal-form bisimilarity for state. In Mikolaj Bojanczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Pra...

    work page doi:10.1007/978-3-030-17127-8 2019

  30. [31]

    A semantical and operational account of call-by-value solvability

    Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability. In Anca Muscholl, editor, Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5...

    work page doi:10.1007/978-3-642-54830-7 2014

  31. [32]

    The duality of computation

    Pierre - Louis Curien and Hugo Herbelin. The duality of computation. In Martin Odersky and Philip Wadler, editors, Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), Montreal, Canada, September 18-21, 2000 , pages 233--243. ACM , 2000. https://doi.org/10.1145/351240.351262 doi:10.1145/351240.351262

    work page doi:10.1145/351240.351262 2000

  32. [33]

    S\'emantiques de la logique lin\'eaire et temps de calcul

    Daniel de Carvalho. S\'emantiques de la logique lin\'eaire et temps de calcul . T h\`ese de doctorat, Universit\'e Aix-Marseille II, 2007

    work page 2007

  33. [34]

    Execution time of \( \) -terms via denotational semantics and intersection types

    Daniel de Carvalho. Execution time of \( \) -terms via denotational semantics and intersection types. Mathematical Structures in Computer Science , 28(7):1169--1203, 2018. https://doi.org/10.1017/S0960129516000396 doi:10.1017/S0960129516000396

    work page doi:10.1017/s0960129516000396 2018

  34. [35]

    The weak lambda calculus as a reasonable machine

    Ugo Dal Lago and Simone Martini. The weak lambda calculus as a reasonable machine. Theor. Comput. Sci. , 398(1-3):32--50, 2008. https://doi.org/10.1016/j.tcs.2008.01.044 doi:10.1016/j.tcs.2008.01.044

    work page doi:10.1016/j.tcs.2008.01.044 2008

  35. [36]

    The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value

    Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In James Cheney and Germ \' a n Vidal, editors, Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016 , pages 174--187. ACM , 2016. h...

    work page doi:10.1145/2967973.2968608 2016

  36. [37]

    Collapsing non-idempotent intersection types

    Thomas Ehrhard. Collapsing non-idempotent intersection types. In Patrick C \' e gielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France , volume 16 of LIPIcs , pages 259--273. Schloss Dagstuhl - Leibniz-Zentrum f \" u r Infor...

    work page doi:10.4230/lipics.csl.2012.259 2012

  37. [38]

    Lambda calculus and probabilistic computation

    Claudia Faggian and Simona Ronchi Della Rocca. Lambda calculus and probabilistic computation. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019 , pages 1--13. IEEE , 2019. https://doi.org/10.1109/LICS.2019.8785699 doi:10.1109/LICS.2019.8785699

    work page doi:10.1109/lics.2019.8785699 2019

  38. [39]

    Discovering needed reductions using type theory

    Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C. Mitchell, editors, Theoretical Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings , volume 789 of Lecture Notes in Computer Science , pages 555--574. Springer, 1994. https://doi.org/10.1007/3-540-57887...

    work page doi:10.1007/3-540-57887-0 1994

  39. [40]

    J.R. Hindley. The Church-Rosser Property and a Result in Combinatory Logic . PhD thesis, University of Newcastle-upon-Tyne, 1964

    work page 1964

  40. [41]

    Milner's lambda calculus with partial substitutions

    Delia Kesner and Shane \'O Conch \'u ir. Milner's lambda calculus with partial substitutions. Technical report, Paris 7 University, 2008. http://www.pps.univ-paris-diderot.fr/ kesner/papers/shortpartial.pdf

    work page 2008

  41. [42]

    Reasoning about call-by-need by means of types

    Delia Kesner. Reasoning about call-by-need by means of types. In Bart Jacobs and Christof L \" o ding, editors, Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016,...

    work page doi:10.1007/978-3-662-49630-5 2016

  42. [43]

    A. J. Kfoury. A linearization of the lambda-calculus and consequences. J. Log. Comput. , 10(3):411--436, 2000. https://doi.org/10.1093/LOGCOM/10.3.411 doi:10.1093/LOGCOM/10.3.411

    work page doi:10.1093/logcom/10.3.411 2000

  43. [44]

    Axel Kerinec, Giulio Manzonetto, and Simona Ronchi Della Rocca. Call-by-value, again! In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference) , volume 195 of LIPIcs , pages 7:1--7:18. Schloss Dagstuhl - Leibniz-Zentrum f \" u r In...

    work page doi:10.4230/lipics.fscd.2021.7 2021

  44. [45]

    The spirit of node replication

    Delia Kesner, Lo \" c Peyrot, and Daniel Ventura. The spirit of node replication. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembour...

    work page doi:10.1007/978-3-030-71995-1 2021

  45. [46]

    Call-by-need, neededness and all that

    Delia Kesner, Alejandro R \' os, and Andr \' e s Viso. Call-by-need, neededness and all that. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Gre...

    work page doi:10.1007/978-3-319-89366-2 2018

  46. [47]

    Quantitative types for the linear substitution calculus

    Delia Kesner and Daniel Ventura. Quantitative types for the linear substitution calculus. In Josep D \' az, Ivan Lanese, and Davide Sangiorgi, editors, Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference, TCS 2014, Rome, Italy, September 1-3, 2014. Proceedings , volume 8705 of Lecture Notes in Computer Science , pages 296--310. Sp...

    work page doi:10.1007/978-3-662-44602-7 2014

  47. [48]

    Abella sources for the proofs of strong bisimulation of structural reductions

    Adrienne Lancelot and Beniamino Accattoli. Abella sources for the proofs of strong bisimulation of structural reductions. GitHub repository, 2025. https://github.com/baccattoli/abella-devs/tree/main/call-by-silly

    work page 2025

  48. [49]

    \'E tude de la polarisation en logique

    Olivier Laurent. \'E tude de la polarisation en logique . Th\`ese de doctorat, U niversit\'e A ix- M arseille II , March 2002

    work page 2002

  49. [50]

    Call-by-push-value: Decomposing call-by-value and call-by-name

    Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. High. Order Symb. Comput. , 19(4):377--414, 2006. https://doi.org/10.1007/s10990-006-0480-6 doi:10.1007/s10990-006-0480-6

    work page doi:10.1007/s10990-006-0480-6 2006

  50. [51]

    Local bigraphs and confluence: Two conjectures: (extended abstract)

    Robin Milner. Local bigraphs and confluence: Two conjectures: (extended abstract). In Roberto M. Amadio and Iain Phillips, editors, Proceedings of the 13th International Workshop on Expressiveness in Concurrency, EXPRESS 2006, Bonn, Germany, August 26, 2006 , volume 175 of Electronic Notes in Theoretical Computer Science , pages 65--73. Elsevier, 2006. ht...

    work page doi:10.1016/j.entcs.2006.07.035 2006

  51. [52]

    Turner, and Philip Wadler

    John Maraist, Martin Odersky, David N. Turner, and Philip Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theor. Comput. Sci. , 228(1-2):175--210, 1999. https://doi.org/10.1016/S0304-3975(98)00358-2 doi:10.1016/S0304-3975(98)00358-2

    work page doi:10.1016/s0304-3975(98)00358-2 1999

  52. [53]

    New semantical insights into call-by-value \( \) -calculus

    Giulio Manzonetto, Michele Pagani, and Simona Ronchi Della Rocca. New semantical insights into call-by-value \( \) -calculus. Fundam. Informaticae , 170(1-3):241--265, 2019. https://doi.org/10.3233/FI-2019-1862 doi:10.3233/FI-2019-1862

    work page doi:10.3233/fi-2019-1862 2019

  53. [54]

    Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci. , 1(2):125--159, 1975. https://doi.org/10.1016/0304-3975(75)90017-1 doi:10.1016/0304-3975(75)90017-1

    work page doi:10.1016/0304-3975(75)90017-1 1975

  54. [55]

    R \' e v \' e sz

    Gy \" o rgy E. R \' e v \' e sz. A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem. Theor. Comput. Sci. , 93(1):75--89, 1992. https://doi.org/10.1016/0304-3975(92)90212-X doi:10.1016/0304-3975(92)90212-X

    work page doi:10.1016/0304-3975(92)90212-x 1992

  55. [56]

    On the relations between the syntactic theories of lambda-mu-calculi

    Alexis Saurin. On the relations between the syntactic theories of lambda-mu-calculi. In Michael Kaminski and Simone Martini, editors, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, Bertinoro, Italy, September 16-19, 2008. Proceedings , volume 5213 of Lecture Notes in Computer Science , pages 154--168. S...

    work page doi:10.1007/978-3-540-87531-4 2008

  56. [57]

    Kristian St vring and S ren B. Lassen. A complete, co-inductive syntactic theory of sequential control and state. In Jens Palsberg, editor, Semantics and Algebraic Specification, Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday , volume 5700 of Lecture Notes in Computer Science , pages 329--375. Springer, 2009. https://doi.org/10.1...

    work page doi:10.1007/978-3-642-04164-8 2009

  57. [58]

    Wadsworth

    Christopher P. Wadsworth. Semantics and pragmatics of the lambda-calculus . Ph D Thesis , Oxford, 1971

    work page 1971