Document Open Access Logo

Modal Embeddings and Calling Paradigms

Authors José Espírito Santo , Luís Pinto , Tarmo Uustalu

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2019.18.pdf
  • Filesize: 0.54 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Program semantics
Keywords
  • intuitionistic S4
  • call-by-name
  • call-by-value
  • comonadic lambda-calculus
  • standardization
  • indifference property

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

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.

Cite As Get BibTex

José Espírito Santo, Luís Pinto, and Tarmo Uustalu. Modal Embeddings and Calling Paradigms. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.18

Author Details

José Espírito Santo
  • Centre of Mathematics, University of Minho, Portugal
Luís Pinto
  • Centre of Mathematics, University of Minho, Portugal
Tarmo Uustalu
  • School of Computer Science, Reykjavik University, Iceland
  • Dept. of Software Science, Tallinn University of Technology, Estonia

Funding

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.

References

  1. H.P. Barendregt. The Lambda Calculus. North-Holland, 1984. Google Scholar
  2. G. M. Bierman and V. C. V. de Paiva. On an intuitionistic modal logic. Studia Logica, 65:383-416, 2000. Google Scholar
  3. 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. Google Scholar
  4. J.-Y. Girard. Linear logic. Theor. Comput. Sci., 50(1):1-102, 1987. Google Scholar
  5. J. Hatcliff and O. Danvy. Thunks and the λ-calculus. J. Funct. Program., 7(3):303-319, 1997. Google Scholar
  6. J. Hatcliff and O. Danvy. Thunks and the λ-Calculus (Extended Version). Technical Report BRICS RS-97-7, DIKU, 1997. Google Scholar
  7. 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. Google Scholar
  8. Ralph Loader. Notes on simply typed lambda calculus. Technical Report ECS-LFCS-98-381, LFCS, Univ. of Edinburgh, 1998. Google Scholar
  9. I. Mackie. The Geometry of Implementation. PhD thesis, Imperial College, 1994. Google Scholar
  10. 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. Google Scholar
  11. 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. Google Scholar
  12. G. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theor. Comput. Sci., 1:125-159, 1975. Google Scholar
  13. D. Prawitz. Natural Deduction. Almquist and Wiksell, Stockholm, 1965. Google Scholar
  14. A. Sabry and P. Wadler. A reflection on call-by-value. ACM Trans. Program. Lang. Syst., 19(6):916-941, 1997. Google Scholar
  15. A. Troelstra. Introductory note to 1933f. In Kurt Gödel Collected Works, pages 296-299. Oxford Univ. Press, 1986. Google Scholar
  16. A. Troelstra and H. Schwichtenberg. Basic Proof Theory. Cambridge Univ. Press, 2000. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact