.png)
On the 7th of January, Danya Rogozin participated in the conference Logical Foundation of Computer Science, Miami, Deerfield Beach. LFCS is a logical and computer science conference, topics of which cover such areas as constructive mathematics, type theory, proof theory, foundations of mathematics, etc.
Danya gave a talk on the results that he obtained in his thesis two years ago. The title is Modal Type Theory Based on the Intuitionistic Modal Logic . This logic was introduced by Sergei Artemov and Tudor Protopopescu to solve some issues related to constructive aspects of agent knowledge and belief.
Considering modal logic from a computational perspective
This logic was considered from a computational perspective. It’s a quite curious coincidence that axioms of this logic are pretty similar to the types of methods pure and (<*>) in the Applicative class well-known in Haskell. In this work, he considered the modal typed lambda calculus that is Curry-Howard isomorphic to the logic and shown such metatheoretical properties as subject reduction, strong normalisation, and confluence.
To get a closer look, you may check out the proceedings book, where the articles based on the speakers’ talks are fully presented.
Also, if you want to read some of Danya’s introductory work about modal logic, feel free to head to his excellent post series on our blog. In it, he covers the basics of modal logic and explores its connections to fields such as computer science, topology, and foundations of mathematics.
