Oratrice: Liron Cohen (Ben-Gurion)
Quand: le lundi 24 février 2025 de 16 h à 17 h
Où: PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy.

Résumé: 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.