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

Title:	Plotkin's call-by-value λ-calculus as a modal calculus
Author:	Espírito Santo, José Pinto, Luís Uustalu, Tarmo orcid.org/0000-0002-1297-0579 3 authors Show fewer authors
Date:	2022-06
Language:	English
Scope:	art. 100775
University/Institute:	Reykjavik University Háskólinn í Reykjavík
School:	School of Technology (RU) Tæknisvið (HR)
Department:	Department of Computer Science (RU) Tölvunarfræðideild (HR)
ISSN:	2352-2208 2352-2216
DOI:	10.1016/j.jlamp.2022.100775
Subject:	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
Show full item record
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.