2026-07-23T17:34:59Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:10525 2024-03-06T10:46:08Z ddc:004 open_access

Modal Embeddings and Calling Paradigms Espírito Santo, José Pinto, Luís Uustalu, Tarmo intuitionistic S4 call-by-name call-by-value comonadic lambda-calculus standardization indifference property We study the computational interpretation of the two standard modal embeddings, usually named after Girard and Gödel, of intuitionistic logic into IS4. As source system we take either the call-by-name (cbn) or the call-by-value (cbv) lambda-calculus with simple types. The target system can be taken to be the, arguably, simplest fragment of IS4, here recast as a very simple lambda-calculus equipped with an indeterminate lax monoidal comonad. A slight refinement of the target and of the embeddings shows that: the target is a calculus indifferent to the calling paradigms cbn/cbv, obeying a new paradigm that we baptize call-by-box (cbb), and enjoying standardization; and that Girard’s (resp. Gödel’s) embbedding is a translation of cbn (resp. cbv) lambda-calculus into this calculus, using a compilation technique we call protecting-by-a-box, enjoying the preservation and reflection properties known for cps translations - but in a stronger form that allows the extraction of standardization for cbn or cbv as consequence of standardization for cbb. The modal target and embeddings achieve thus an unification of call-by-name and call-by-value as call-by-box. Schloss Dagstuhl – Leibniz-Zentrum für Informatik José Espírito Santo and Luís Pinto and Tarmo Uustalu 2019 Is Part Of LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2019.18 urn:nbn:de:0030-drops-105256 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.18 eng https://creativecommons.org/licenses/by/3.0/legalcode