Plotkin's call-by-value λ-calculus as a modal calculus

Titill:	Plotkin's call-by-value λ-calculus as a modal calculus
Höfundur:	Espírito Santo, José Pinto, Luís Uustalu, Tarmo orcid.org/0000-0002-1297-0579 3 höfundar Sýna færri höfunda
Útgáfa:	2022-06
Tungumál:	Enska
Umfang:	art. 100775
Háskóli/Stofnun:	Reykjavik University Háskólinn í Reykjavík
Svið:	School of Technology (RU) Tæknisvið (HR)
Deild:	Department of Computer Science (RU) Tölvunarfræðideild (HR)
ISSN:	2352-2208 2352-2216
DOI:	10.1016/j.jlamp.2022.100775
Efnisorð:	Software; Theoretical Computer Science; Computational Theory and Mathematics; Logic; lambda-calculus; call-by-name; call-by-value; S4 modal logic; Girard's embedding; Gödel's embedding
URI:	https://hdl.handle.net/20.500.11815/4745
Skoða fulla færslu
Útdráttur: In 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.