More on Modal Embeddings and Calling Paradigms
University of Minho
Abstract: We recapitulate our work on the computational interpretation of the two main embeddings of intuitionistic logic into modal logic S4, often attributed to Girard and Goedel. They are interpreted as compilations of, respectively, the call-by-name and Plotkin's call-by-value lambda-calculus into a simple modal target - a lambda-calculus following a new calling paradigm, named "call-by-box", enjoying a property of standardization based on a notion of "weak and external" evaluation. The modal embeddings unify the well-known calling paradigms by the novel one, as they show how the respective standardization theorems follow from the same property of the modal target. In a recent work, we improved on this picture. A refinement of the modal target reveals the coexistence of two modes of reduction, both following (and unified by) call-by-box, distinguished by modal reasons, but nevertheless linked to call-by-name and call-by-value. The modal embeddings now become the isomorphisms which allow us to see the connection between the well-known calling paradigms and the two modes of reduction hidden inside modal logic S4.
Joint work with Luís Pinto and Tarmo Uustalu.