PoP Seminar - Liron Cohen
May 14, 2026 11:00AM—12:00PM
Location:
In Person
-
Traffic21 Classroom, Gates Hillman 6501
Speaker:
LIRON COHEN,
Associate Professor, Institute for the Theory of Computing, Faculty of Computer and Information Science, Ben-Gurion University
https://www.lironcohenlab.com/
First-Class Effects: A Unified Effectful Type Theory for Continuity, Choice, and Search
Thursday, May 14, 2026, 11am – 12pm 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.
—
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.
Faculty Host: Stephanie Balzer
Event Type: Seminars
Room Number: In Person
Building: Traffic21 Classroom, Gates Hillman 6501
Speaker's Name: LIRON COHEN
Speaker Website: www.lironcohenlab.com
Speaker's Professional Title: Associate Professor, Institute for the Theory of Computing Faculty of Computer and Information Science, Ben-Gurion University
Talk Title: First-Class Effects: A Unified Effectful Type Theory for Continuity, Choice, and Search
For More Information: mstanle2@andrew.cmu.edu
Affiliations: Computer Science Department (CSD)
Organization(s): School of Computer Science
Event Website Title: Series Website
Event Website URL: www.cs.cmu.edu…
For More Information:
mstanle2@andrew.cmu.edu