Event Title: Modal (Propositions as Types)

Speaker: Nachiappan (Nachi) Valliappan

Dates: Thursday, 27^th November 2025

Time: 11am (GMT)

Location: Edinburgh Bayes Coffee House (4^th floor Bayes Center, EH8 9BT)

Join Online：https://app.huawei.com/wmeeting/join/97172374/EBLvR69PyCciIQAbMEtNCHM4PJYNA1XrY

Meeting ID：97172374

Passcode：507513

Talk Abstract:

“Propositions as types” is a slogan that refers to the one-to-one correspondence between propositions in formal logic and types in programming language theory. The discovery of this correspondence in the twentieth century opened the gates for cross-disciplinary exchange of ideas and has since had an enormous impact on the mutual development of formal verification tools and programming languages. In recent times, however, programming language research has seen a rise in the development of so-called “modal” types whose status is yet to be settled from the perspective of logic. These appear, at the surface level, an awful lot like modalities in modal logic, but much has remained unclear on the matter. This gap in the propositions-as-types correspondence is a lost opportunity: modal logics enjoy a rich suite of analysis tools that could be readily ported to modal type systems via the correspondence. This talk is about ongoing research in the conjunction of intuitionistic modal logic and programming languages to bridge this gap, and the potential applications of this research in modular program transformation and security analyses.

Speaker:
Nachiappan (Nachi) Valliappan is a Royal Society Newton International Fellow in the Laboratory for Foundations of Computer Science at the University of Edinburgh.

【Edinburgh Bayes Coffee House Tech Talk】Modal (Propositions as Types) / Huawei-Edinburgh Joint Lab by blogadmin is licensed under a Creative Commons Attribution CC BY 3.0