Serokell at LCFS 2020

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.

Banner that links to Serokell Shop. You can buy hip FP T-shirts there!
More from Serokell
Serokell at FPure 2019Serokell at FPure 2019
Functional Futures by Serokell among Best Functional Programming PodcastsFunctional Futures by Serokell among Best Functional Programming Podcasts
Serokell at NixCon 2020Serokell at NixCon 2020