Por José Carlos Espírito Santo (Centro de Matemática, Universidade do Minho).
Abstract: We study the computational interpretation of the two standard embeddings, usually named after Girard and Gödel, of intuitionistic logic into modal logic IS4, and show that the embeddings are translations between calling paradigms of functional programming. To this effect, the common target system of the embeddings 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. As the source system we take respectively the call-by-name (cbn) and the call-by-value (cbv) lambda-calculus with simple types. Unlike cps translations, which translate cbn and cbv into each other, the modal embeddings unify cbn and cbv as call-by-box (cbb), a new paradigm identified in the target fragment of IS4. The technical justification of such unification is the standardization theorem for cbb, from which we extract the standardization theorems for cbn and cbv as corollaries, with the help of the properties of the modal embeddings. These results are both stronger and more abstract than those known of embeddings into linear logic.
(Joint work with Luís Pinto and Tarmo Uustalu)
