A Contextual Formalization of Coinduction

Speaker: Paul Downen (UMass Lowell)
When: Friday, February 27 2026, 16:00–17:00
Where: Room PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy

Abstract: Every day, a large community of computer scientists — working on applications and theory of functional programming, verification, type systems, and semantics — employs induction to effectively reason about software and its behavior. Whether mechanically checked by a computer or informally written with pen and paper, various forms of inductive techniques are applied with confidence that the result is well-founded. What is the secret to confidence? The inductive principle itself limits recursive reasoning to only pieces of the original example which are structurally smaller than it.

Coinduction, in contrast, is not nearly as well-understood or used as its dual, induction. This is not because coinduction is less useful than induction: many important software systems like concurrent processes, web servers, and operating systems are naturally coinductive. Why, then, does coinduction see less use in both informally-written and mechanically-verified proofs of programming language theory? One major obstacle is that coinduction is easy to formulate in a dangerous way, where the recursive nature of coinduction seems too powerful on the surface and can lead to nonsensical, viciously circular proofs. To tame this unreasonable power, in practice, we must externally check that the coinductive hypothesis is only applied in certain special contexts, which fundamentally breaks compositional reasoning, where a certain proof may seem valid until it is embedded into a larger context.

In this talk, we will consider how to alleviate this difficulty with coinduction by rephrasing it in a way that more closely resembles the familiar and comfortable forms of formal and informal induction used in practice. Our methodology is to work in a setting where the important contexts are reified into first-class objects that can be labeled and have a predictable structure — similar to inductive objects like numbers and trees, which can be named and analyzed structurally. Together with the notion of copattern matching already used in some proof assistants, the key idea is that the coinductive principle limits recursion to only contexts which are structurally smaller than the starting point of coinduction, and that this requirement is checked locally by just looking at the label where recursion happens. This talk discusses a new principle of coinduction — in terms of both an informal pen-and-paper methodology as well as a formal type system for proving equality of corecursive programs with or without side effects — based on the idea that coinduction can be seen as induction on the context. Both the informal technique and formal system are proven consistent with a computational model where every syntactically-derived equality is a proof of observational equivalence.

Aeneas: Formal Verification of Rust programs by Functional Translation

Speaker: Aymeric Fromherz (Inria)
When: Wednesday, April 30 2025, 16:00–17:00
Where: Room PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy
Slides: PDF

Abstract: The Rust programming language has recently gained traction in industrial settings and in the systems community. A large part of this success stems from several key features of the language: Rust provides both the high performance and low-level idioms commonly associated to languages like C and C++, as well as memory safety by default thanks to its rich, borrow-based type system. However, despite being safer than C or C++, Rust programs are not immune to bugs and vulnerabilties, including aborted executions (i.e., Rust’s panic), incorrect uses of the unsafe escape hatch, or simply programs that do not match their expected behaviour, raising the need for novel static analyzers and verification tools.

To this end, we present Aeneas, a new toolchain geared towards the formal verification of Rust programs. Aeneas leverages Rust’s region-based type system to eliminate memory reasoning for a large class of Rust programs: relying on a custom borrow-centric symbolic execution, the toolchain translates safe Rust programs to a semantically equivalent functional model in proof assistants such as Lean, Rocq, or F*, enabling the use of powerful logics to specify and reason about programs.

In this talk, we will show the core ideas behind Aeneas’ functional translation on several examples, and present the broader ecosystem around Aeneas, including the Charon analysis framework and ongoing work on transpilers between C and Rust to handle legacy systems.

Student talks: Genesse, Huberdeau and Sano

MAPLS has been rebranded to LLM: thanks to Jean Privat for the suggested rebranding!

Speakers: Hugo Genesse (UQAM), Laurent Huberdeau (Université de Montréal) and Chuta Sano (McGill University)
When: Monday, March 31 2025, 16:00–17:00
Where: Room PK-5115, Pavillon Président-Kennedy (UQAM), 201 avenue du Président-Kennedy.

Effectful Curry-Howard

Please join us for the first MAPLS seminar talk!

Title: Effectful Curry-Howard
Speaker: Liron Cohen (Ben-Gurion)
When: Monday, February 24 2025, 16:00–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.