Modal Embeddings and Calling Paradigms
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.
intuitionistic S4
call-by-name
call-by-value
comonadic lambda-calculus
standardization
indifference property
Theory of computation~Logic
Theory of computation~Program semantics
18:1-18:20
Regular Paper
J.E.S. and L.P. were supported by Fundação para a Ciência e a Tecnologia (FCT) through project UID/MAT/00013/2013. T.U. was supported by the Estonian Ministry of Education and Research through institutional research grant IUT33-13. All three authors received support from the COST action CA15123 EUTYPES.
José
Espírito Santo
José Espírito Santo
Centre of Mathematics, University of Minho, Portugal
https://orcid.org/0000-0002-6348-5653
Luís
Pinto
Luís Pinto
Centre of Mathematics, University of Minho, Portugal
https://orcid.org/0000-0003-1338-2688
Tarmo
Uustalu
Tarmo Uustalu
School of Computer Science, Reykjavik University, Iceland
Dept. of Software Science, Tallinn University of Technology, Estonia
https://orcid.org/0000-0002-1297-0579
10.4230/LIPIcs.FSCD.2019.18
H.P. Barendregt. The Lambda Calculus. North-Holland, 1984.
G. M. Bierman and V. C. V. de Paiva. On an intuitionistic modal logic. Studia Logica, 65:383-416, 2000.
T. Ehrhard and G. Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In Proc. of PPDP '16, pages 174-187. ACM, 2016.
J.-Y. Girard. Linear logic. Theor. Comput. Sci., 50(1):1-102, 1987.
J. Hatcliff and O. Danvy. Thunks and the λ-calculus. J. Funct. Program., 7(3):303-319, 1997.
J. Hatcliff and O. Danvy. Thunks and the λ-Calculus (Extended Version). Technical Report BRICS RS-97-7, DIKU, 1997.
Y. Lafont. From proof-nets to interaction nets. In J. Y. Girard, Y. Lafont, and L. Regnier, editors, Advances in Linear Logic, pages 225-247. Cambridge Univ. Press, 1995.
Ralph Loader. Notes on simply typed lambda calculus. Technical Report ECS-LFCS-98-381, LFCS, Univ. of Edinburgh, 1998.
I. Mackie. The Geometry of Implementation. PhD thesis, Imperial College, 1994.
I. Mackie. Encoding strategies in the lambda calculus with interaction nets. In Revised Selected Papers from IFL 2005, volume 4015 of Lect. Notes in Comput. Sci., pages 19-36. Springer, 2006.
J. Maraist, M. Odersky, D. N. Turner, and P. Wadler. Call-by-name, call-by-value, call-by-need and the linear lambda calculus. Theor. Comput. Sci., 228(1-2):175-210, 1999.
G. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theor. Comput. Sci., 1:125-159, 1975.
D. Prawitz. Natural Deduction. Almquist and Wiksell, Stockholm, 1965.
A. Sabry and P. Wadler. A reflection on call-by-value. ACM Trans. Program. Lang. Syst., 19(6):916-941, 1997.
A. Troelstra. Introductory note to 1933f. In Kurt Gödel Collected Works, pages 296-299. Oxford Univ. Press, 1986.
A. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge Univ. Press, 2000.
José Espírito Santo, Luís Pinto, and Tarmo Uustalu
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode