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.

About the speaker: Paul Downen is an Assistant Professor in the Miner School of Computer & Information Sciences at University of Massachusetts, Lowell since Fall 2021. Previously, he completed his Ph.D. from the University of Oregon’s Department of Computer and Information Science. his general research interests are in the study of programming languages, including their theory, semantics, design, and implementation, with a focus on the foundations of computation and its relation to logic and duality.