Serokell at LCFS 2020

Gints DreimanisDanya Rogozin
January 17th, 2020
1 min read

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.

logical foundations of computer science

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 IEL{\bf IEL}^{-}. 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 IEL{\bf IEL}^{-} 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.

Serokell at LCFS 2020
More from Serokell
Serokell among the top AI developersSerokell among the top AI developers
Watch Programming Lectures from Serokell AcademyWatch Programming Lectures from Serokell Academy
Serokell Launches a Scholarship Together With ITMOSerokell Launches a Scholarship Together With ITMO