Last year, Daniel Rogozin participated in a conference called Logical Foundations of Computer Science (Miami, USA, 2020). The contribution was the conference paper and lecture on the computational interpretation of some intuitionistic modal logics. For more info, check this brief report about the conference.
The extended paper has been recently released in the Journal of Logic and Computation (Oxford University Press). The previous article was about questions related to syntax. In other words, Daniel was considering the modal typed lambda calculus based on the curious system of intuitionistic modal logic where he proved such properties as confluence and strong normalization.
The extended paper covers a broader class of topics. In addition to syntax, Daniel also proposed semantic analysis of those intuitionistic modal logics. In this paper, he proved that the obtained modal lambda calculus is complete with respect to cartesian closed categories equipped with coalgebras obtained from the monoidal endofunctor. That provides essential categorical intuition for evaluation in this type theory.
Additionally, he analyzed a class of logics by means of Kripke-Joyal semantics. This kind of semantics arose from topos theory and generalisation of the underlying topological notions proposed by Grothendieck. The modalities might be interpreted as prenuclear operators used in point-free topology. This version of topology studies topological spaces as lattices of open neighbourhoods without mentioning geometric points. As Newton said: “if I have seen further, it is by standing on the shoulders of Giants”. This aphorism illustrates the paper since this part of the article develops Robert Goldblatt’s ideas.
The paper is available online, and it is to appear in the special issue of the Journal of Logic and Computation prepared by Sergei Artemov (City University of New York) and Anil Nerode (Cornell University).
