Document Open Access Logo

Lax Modal Lambda Calculi

Author Nachiappan Valliappan

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2026.46.pdf
  • Filesize: 1.08 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Modal and temporal logics
Keywords
  • intuitionistic modal logic
  • typed lambda calculi
  • diamond modality

Metrics

Abstract

Intuitionistic modal logics (IMLs) extend intuitionistic propositional logic with modalities such as the box and diamond connectives. Advances in the study of IMLs have inspired several applications in programming languages via the development of corresponding type theories with modalities. Until recently, IMLs with diamonds have been misunderstood as somewhat peculiar and unstable, causing the development of type theories with diamonds to lag behind type theories with boxes. In this article, we develop a family of typed-lambda calculi corresponding to sublogics of a peculiar IML with diamonds known as Lax logic. These calculi provide a modal logical foundation for various strong functors in typed-functional programming. We present possible-world and categorical semantics for these calculi and constructively prove normalization, equational completeness and proof-theoretic inadmissibility results. Our main results have been formalized using the proof assistant Agda.

Cite As Get BibTex

Nachiappan Valliappan. Lax Modal Lambda Calculi. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 46:1-46:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CSL.2026.46

Author Details

Nachiappan Valliappan
  • University of Edinburgh, UK

Funding

This work was funded by a Royal Society Newton International Fellowship.

Acknowledgements

I thank Alex Kavvos, Andreas Abel, Carlos Tomé Cortiñas, Fabian Ruch and my colleagues at the University of Edinburgh for their feedback on this work. I also thank the anonymous reviewers of this paper and its previous versions for their valuable comments and suggestions.

Supplementary Materials

References

  1. Andreas Abel, Guillaume Allais, Jesper Cockx, Nils Anders Danielsson, Philipp Hausmann, Fredrik Nordvall Forsberg, Ulf Norell, Víctor López Juan, Andrés Sicard-Ramírez, and Andrea Vezzosi. Agda 2. URL: https://wiki.portal.chalmers.se/agda/pmwiki.php.
  2. Danel Ahman. When programs have to watch paint dry. In Orna Kupferman and Pawel Sobocinski, editors, Foundations of Software Science and Computation Structures - 26th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, volume 13992 of Lecture Notes in Computer Science, pages 1-23. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30829-1_1.
  3. Natasha Alechina, Michael Mendler, Valeria de Paiva, and Eike Ritter. Categorical and kripke semantics for constructive S4 modal logic. In Laurent Fribourg, editor, Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings, volume 2142 of Lecture Notes in Computer Science, pages 292-307. Springer, 2001. URL: https://doi.org/10.1007/3-540-44802-0_21.
  4. Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings, pages 303-310. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/LICS.2001.932506.
  5. Patrick Bahr, Christian Graulund, and Rasmus Ejlers Møgelberg. Simply ratt: a fitch-style modal calculus for reactive programming without space leaks. Proc. ACM Program. Lang., 3(ICFP):109:1-109:27, 2019. URL: https://doi.org/10.1145/3341713.
  6. Philippe Balbiani, Han Gao, Çigdem Gencer, and Nicola Olivetti. A natural intuitionistic modal logic: Axiomatization and bi-nested calculus. In Aniello Murano and Alexandra Silva, editors, 32nd EACSL Annual Conference on Computer Science Logic, CSL 2024, February 19-23, 2024, Naples, Italy, volume 288 of LIPIcs, pages 13:1-13:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CSL.2024.13.
  7. P. N. Benton, Gavin M. Bierman, and Valeria de Paiva. Computational types from a logical perspective. J. Funct. Program., 8(2):177-193, 1998. URL: https://doi.org/10.1017/s0956796898002998.
  8. Ulrich Berger, Matthias Eberl, and Helmut Schwichtenberg. Normalization by evaluation. Prospects for Hardware Foundations: ESPRIT Working Group 8533 NADA—New Hardware Design Methods Survey Chapters, pages 117-137, 1998. Google Scholar
  9. Ulrich Berger and Helmut Schwichtenberg. An inverse of the evaluation functional for typed lambda-calculus. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pages 203-211. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/LICS.1991.151645.
  10. Aleš Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus E. Møgelberg, and Lars Birkedal. Guarded dependent type theory with coinductive types. In Bart Jacobs and Christof Löding, editors, Foundations of Software Science and Computation Structures, pages 20-35, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. Google Scholar
  11. Valentijn Anton Johan Borghuis. Coming to terms with modal logic. Technische Universiteit Eindhoven, Eindhoven, 1994. On the interpretation of modalities in typed λ-calculus, Dissertation, Technische Universiteit Eindhoven, Eindhoven, 1994. Google Scholar
  12. Milan Božić and Kosta Došen. Models for normal intuitionistic modal logics. Studia Logica, 43(3):217-245, 1984. URL: https://doi.org/10.1007/BF02429840.
  13. Ranald Clouston. Fitch-style modal lambda calculi. In Christel Baier and Ugo Dal Lago, editors, Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10803 of Lecture Notes in Computer Science, pages 258-275. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_14.
  14. Catarina Coquand. From semantics to rules: A machine assisted analysis. In Egon Börger, Yuri Gurevich, and Karl Meinke, editors, Computer Science Logic, 7th Workshop, CSL '93, Swansea, United Kingdom, September 13-17, 1993, Selected Papers, volume 832 of Lecture Notes in Computer Science, pages 91-105. Springer, 1993. URL: https://doi.org/10.1007/BFB0049326.
  15. Catarina Coquand. A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions. High. Order Symb. Comput., 15(1):57-90, 2002. URL: https://doi.org/10.1023/A:1019964114625.
  16. Anupam Das and Sonia Marin. On intuitionistic diamonds (and lack thereof). In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September 18-21, 2023, Proceedings, volume 14278 of Lecture Notes in Computer Science, pages 283-301. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-43513-3_16.
  17. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. J. ACM, 48(3):555-604, May 2001. URL: https://doi.org/10.1145/382780.382785.
  18. Jim de Groot, Ian Shillito, and Ranald Clouston. Semantical analysis of intuitionistic modal logics between CK and IK. In 40th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2025, Singapore, June 23-26, 2025, pages 169-182. IEEE, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00020.
  19. Wojciech Dzik, Jouni Järvinen, and Michiro Kondo. Intuitionistic propositional logic with galois connections. Log. J. IGPL, 18(6):837-858, 2010. URL: https://doi.org/10.1093/JIGPAL/JZP057.
  20. Matt Fairtlough and Michael Mendler. Propositional lax logic. Inf. Comput., 137(1):1-33, 1997. URL: https://doi.org/10.1006/inco.1997.2627.
  21. Marcelo P. Fiore and Alex K. Simpson. Lambda definability with sums via grothendieck logical relations. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Conference, TLCA'99, L'Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 147-161. Springer, 1999. URL: https://doi.org/10.1007/3-540-48959-2_12.
  22. Gisèle Fischer Servi. On modal logic with an intuitionistic base. Studia Logica, 36(3):141-149, 1977. URL: https://doi.org/10.1007/BF02121259.
  23. Jason Z. S. Hu and Brigitte Pientka. Layered modal type theory. In Stephanie Weirich, editor, Programming Languages and Systems, pages 52-82, Cham, 2024. Springer Nature Switzerland. Google Scholar
  24. G. A. Kavvos. Dual-context calculi for modal logic. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005089.
  25. G. A. Kavvos. Dual-context calculi for modal logic. Log. Methods Comput. Sci., 16(3), 2020. URL: https://doi.org/10.23638/LMCS-16(3:10)2020.
  26. G. A. Kavvos. Two-dimensional kripke semantics II: stability and completeness. CoRR, abs/2406.03578, 2024. URL: https://doi.org/10.48550/arXiv.2406.03578.
  27. Georgios Alexandros Kavvos. Two-dimensional kripke semantics I: presheaves. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction, FSCD 2024, Tallinn, Estonia, July 10-13, 2024, volume 299 of LIPIcs, pages 14:1-14:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.FSCD.2024.14.
  28. Lena Magnusson and Bengt Nordström. The ALF proof editor and its proof engine. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers, volume 806 of Lecture Notes in Computer Science, pages 213-237. Springer, 1993. URL: https://doi.org/10.1007/3-540-58085-9_78.
  29. John C. Mitchell and Eugenio Moggi. Kripke-style models for typed lambda calculus. Ann. Pure Appl. Log., 51(1-2):99-124, 1991. URL: https://doi.org/10.1016/0168-0072(91)90067-V.
  30. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55-92, 1991. URL: https://doi.org/10.1016/0890-5401(91)90052-4.
  31. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. ACM Trans. Comput. Log., 9(3):23:1-23:49, 2008. URL: https://doi.org/10.1145/1352582.1352591.
  32. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci., 11(4):511-540, 2001. URL: https://doi.org/10.1017/S0960129501003322.
  33. Gordon D. Plotkin and Colin Stirling. A framework for intuitionistic modal logics. In Joseph Y. Halpern, editor, Proceedings of the 1st Conference on Theoretical Aspects of Reasoning about Knowledge, Monterey, CA, USA, March 1986, pages 399-406. Morgan Kaufmann, 1986. Google Scholar
  34. Gisèle Fischer Servi. Semantics for a Class of Intuitionistic Modal Calculi, pages 59-72. Springer Netherlands, Dordrecht, 1981. URL: https://doi.org/10.1007/978-94-009-8937-5_5.
  35. Alex K. Simpson. The proof theory and semantics of intuitionistic modal logic. PhD thesis, University of Edinburgh, UK, 1994. URL: https://hdl.handle.net/1842/407.
  36. Vladimir H Sotirov. Modal theories with intuitionistic logic. In Proceedings of the Conference on Mathematical Logic, Sofia, pages 139-171, 1980. Google Scholar
  37. Nachiappan Valliappan. Supplementary material for lax modal lambda calculi. Software, (visited on 2026-02-04). URL: https://github.com/nachivpn/s
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.25486
  38. Nachiappan Valliappan, Fabian Ruch, and Carlos Tom'e Corti nas. Normalization for fitch-style modal calculi. Proc. ACM Program. Lang., 6(ICFP):772-798, 2022. URL: https://doi.org/10.1145/3547649.
  39. Duminda Wijesekera. Constructive modal logics I. Ann. Pure Appl. Log., 50(3):271-301, 1990. URL: https://doi.org/10.1016/0168-0072(90)90059-B.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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