Liron Cohen: Effectful Curry-Howard

Please join us for the first MAPLS seminar talk!

Title: Effectful Curry-Howard
Speaker: Liron Cohen
When: Monday, February 24 2025 from 16:00 to 17:00
Where: Room PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy.

Abstract: The Curry-Howard correspondence and its semantic embodiment in the form of realizability, establish a foundational connection between logic, programming, and type systems. However, these fundamental frameworks fall short of addressing modern computational paradigms that rely on effects such as state, concurrency, and probabilistic behavior. This talk explores effectful Curry-Howard, focusing on extending the Curry-Howard correspondence to integrate computational effects into the framework of realizability. We introduce two new algebraic structures: Evidenced Frames, which provide an abstract structure for building effectful realizability models, and Monadic Combinatory Algebras, a monadic-based extension of traditional partial combinatory algebras. We will see how these extensions not only have a critical impact on the resulting theory, allowing novel computational interpretations of key principles, but also offer a robust framework for verifying modern computational systems.

About the speaker: Liron Cohen is an assistant professor of Computer Science at Ben-Gurion University who uses formal methods to develop frameworks that support formal reasoning about programs and proofs, aiming to improve reliable software and formalized mathematics. Her research focuses on expanding notions of computation and the logical principles governing the properties of systems, as well as developing formal techniques that facilitate program verification and mechanized mathematics. She was a Fulbright postdoctoral researcher at Cornell University, and she received her PhD and MSc from Tel Aviv University.