Reykjavik UniversityHáskólinn í ReykjavíkEspírito Santo, JoséPinto, LuísUustalu, Tarmo2024-02-292024-02-292022-062352-22082352-2216https://hdl.handle.net/20.500.11815/4745In the authors' previous analysis of the calling paradigms call-by-name and call-by-value through Girard's and Gödel's embeddings into the S4 modal logic, an asymmetry remains: the two paradigms are unified by the call-by-box paradigm of the modal target, but only for call-by-name can one say that the paradigm exists, up to isomorphism, inside the modal target. In this paper, we show that, by pushing further the modal analysis, a symmetric situation is revealed, in that ordinary and Plotkin's λ-calculi are shown to truly co-exist inside a simple modal calculus.art. 100775eninfo:eu-repo/semantics/closedAccessSoftwareTheoretical Computer ScienceComputational Theory and MathematicsLogiclambda-calculuscall-by-namecall-by-valueS4 modal logicGirard's embeddingGödel's embeddinginfo:eu-repo/semantics/articleJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2022.100775