Skip to main content
Upcoming Events:

Seminar: Brigitte Pientka, McGill University

Date & Time:
   Add All to Calendar

Zoom meeting:  Please contact the event contact person for details.

Event Contact:

Dr. Spencer Smith  (

Mechanizing Metatheory -- The Next Chapter


Mechanizing formal systems and proofs about them plays an important role in establishing trust in programming languages and verifying software systems in general. Over the past decades, we have seen significant progress and success: the POPLMark challenge popularized the use of proof assistants in mechanizing the metatheory of programming  languages; the development of the first verified compiler in Coq demonstrated the feasibility and value of building verified compilers. Today, mechanizing proofs is a stable fixture in the daily life of programming languages researchers.  One might be tempted to assume that all is well -- yet, the reality is  that we seem to accept the status quo and focus on engineering solutions to get the next job done, although mechanizations can be time consuming and require substantial (sometimes heroic) effort.  In this talk I will argue that we should strive to develop high-level abstractions, primitives, and tools to standardize common tasks and operations arising when working with formal systems and proofs about them.

Taking a look back at some of the foundational theoretical ideas and choices that underly type-theoretic proof environments today, I will survey recent achievements and sketch a dependently typed language that makes it easier to represent, maintain, and communicate formal systems and proofs about them -- an elegant proof language for a more civilized age.


Brigitte Pientka is a Full Professor in the School of Computer Science at McGill University, Montreal, Canada. Her main research interests lie in the area of foundations of programming languages, type theories, and logic. Currently her research focus is on building a type-theoretic foundation for reasoning about formal systems.

B. Pientka honors include a Humboldt Research Fellowship (2016 - 2018) and an Accellerator Award (2012 - 2015) from the Natural Sciences and Engineering Research Council of Canada given to researchers who have an established, superior research program that is highly rated in terms of originality and innovation. In 2018, she received the Test of Time Award from the International Symposium on Principles and Practices of Declarative Programming (PPDP) for her work on the Beluga proof and programming environment. She is presently serving on the editorial board of the Journal of Functional Programming and ACM Transactions on Computational Logic and is an executive editor of the \jour{Logical Methods in Computer Science}. She is also a member of the steering committee of the European Symposium on  Programming (ESOP) and the Symposium on Principles of Programming Languages (POPL).