DROPS

Artifact

Software

Supplementary material for lax modal lambda calculi

Authors: Nachiappan Valliappan

Abstract

Cite as

Nachiappan Valliappan. Supplementary material for lax modal lambda calculi (Software, Formalization). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{Valliappan25,
   title = {{Supplementary material for lax modal lambda calculi}}, 
   author = {Valliappan, Nachiappan},
   note = {Software, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:a7236a3546548ed634ce20cad62755fefaddd77e;origin=https://github.com/nachivpn/s;visit=swh:1:snp:481b2444576d9b650f534269e7768324a916859c;anchor=swh:1:rev:1025664abbf7edbfe7153f9e0ec7250892d4b465}{\texttt{swh:1:dir:a7236a3546548ed634ce20cad62755fefaddd77e}} (visited on 2026-02-18)},
   url = {https://github.com/nachivpn/s},
   doi = {10.4230/artifacts.25486},
}

Document

DOI: 10.4230/LIPIcs.CSL.2026.46

Lax Modal Lambda Calculi

Authors: Nachiappan Valliappan

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

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

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)

Copy BibTex To Clipboard

@InProceedings{valliappan:LIPIcs.CSL.2026.46,
  author =	{Valliappan, Nachiappan},
  title =	{{Lax Modal Lambda Calculi}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{46:1--46:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.46},
  URN =		{urn:nbn:de:0030-drops-254714},
  doi =		{10.4230/LIPIcs.CSL.2026.46},
  annote =	{Keywords: intuitionistic modal logic, typed lambda calculi, diamond modality}
}

Search Results

Documents authored by Valliappan, Nachiappan

Supplementary material for lax modal lambda calculi

Abstract

Cite as

Lax Modal Lambda Calculi

Abstract

Cite as

Thanks for your feedback!

Could not send message