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

Espírito Santo, José; Pinto, Luís; Uustalu, Tarmo

dc.contributor	Reykjavik University
dc.contributor	Háskólinn í Reykjavík
dc.contributor.author	Espírito Santo, José
dc.contributor.author	Pinto, Luís
dc.contributor.author	orcid.org/0000-0002-1297-0579 Uustalu, Tarmo
dc.date.accessioned	2024-02-29T09:44:22Z
dc.date.available	2024-02-29T09:44:22Z
dc.date.issued	2022-06
dc.identifier.issn	2352-2208
dc.identifier.issn	2352-2216
dc.identifier.uri	https://hdl.handle.net/20.500.11815/4745
dc.description.abstract	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.
dc.description.sponsorship	The first and second authors were partially financed by Portuguese Funds through FCT (Fundação para a Ciência e Tecnologia) within the projects UIDB/00013/2020 and UIDP/00013/2020. The third author was supported by the Estonian Ministry of Education and Research institutional research grant IUT33-13 and the Estonian Research Council team grant PRG1210. All the three authors were supported by the EU COST action CA15123 EUTYPES.
dc.format.extent	art. 100775
dc.language.iso	en
dc.publisher	Elsevier BV
dc.rights	info:eu-repo/semantics/closedAccess
dc.subject	Software
dc.subject	Theoretical Computer Science
dc.subject	Computational Theory and Mathematics
dc.subject	Logic
dc.subject	lambda-calculus
dc.subject	call-by-name
dc.subject	call-by-value
dc.subject	S4 modal logic
dc.subject	Girard's embedding
dc.subject	Gödel's embedding
dc.title	Plotkin's call-by-value λ-calculus as a modal calculus
dc.type	info:eu-repo/semantics/article
dc.description.version	Peer Reviewed
dc.identifier.journal	Journal of Logical and Algebraic Methods in Programming
dc.identifier.doi	10.1016/j.jlamp.2022.100775
dc.contributor.department	Department of Computer Science (RU)
dc.contributor.department	Tölvunarfræðideild (HR)
dc.contributor.school	School of Technology (RU)
dc.contributor.school	Tæknisvið (HR)