PoP Seminar Talk

First-Class Effects - A Unified Effectful Type Theory for Continuity, Choice, and Search

Liron Cohen, Associate Professor, Ben-Gurion University
Thursday, 14 May, 2026; 11:00am
GHC 6501
Host: Stephanie Balzer

Abstract

Programming languages usually treat effects with caution: state, failure, nondeterminism, choice, and interaction complicate reasoning and threaten metatheoretic properties. In this talk, I will argue that effects are not merely impurities to be controlled, but first-class semantic capabilities that can reveal and shape the logic of type theory. I will present boxTT, a unified effectful type-theoretic framework in which modalities and choice operators make effects part of the structure of the theory itself. This lets us ask a foundational question: which logical principles become valid when a type theory has certain computational effects and a certain discipline for controlling them? As case studies, I will show how stateful computations can internalize continuity by computing moduli of continuity for higher-order programs over infinite streams, and how effectful models can separate variants of Markov’s principle that correspond to different strengths of search and witness extraction. Ultimately, the aim is to move beyond isolated effectful models toward foundational type theories with native effects, where constructive principles can be systematically validated, separated, and transported according to the computational capabilities available.

Bio

Liron Cohen is an associate professor in the Faculty of Computer and Information Science at Ben-Gurion University and is currently visiting Cornell University. Her research lies at the intersection of programming languages, type theory, constructive mathematics, and proof assistant formalization, where she develops formal frameworks for reasoning about programs and proofs with the broader aim of building foundations for reliable software and formalized mathematics. Her recent work focuses on building semantic and type-theoretic foundations that broaden the notion of computation, especially by making computational effects such as state, choice, nondeterminism, and control part of the foundations of type theory. Her work has appeared in leading venues including JACM, LICS, and POPL, has been recognized by awards such as the BSF Pazy Memorial Research Award, and includes recent verification work that received TACAS 2025 Distinguished Paper and Distinguished Artifact Awards. She was a Fulbright postdoctoral researcher at Cornell University and received her PhD and MSc from Tel Aviv University.