Proof Representations: From Theory to Applications (25w5406)

The Banff International Research Station will host the “Proof Representations: From Theory to Applications” workshop in Banff from June 1 - 6, 2025.

Reasoning is a fundamental part of our everyday lives. Whenever we find ourselves engaged in a debate or attempting to make a case for something, we instinctively begin by gathering the foundational assumptions we believe are true. We then construct a coherent argument based on these assumptions and present our resulting conclusions, building a bridge of ideas from what we believe to what we want to convince others of. Within the realm of formal logic, logicians use logical reasoning to rigorously deduce new insights and conclusions from previously established theorems that have been verified as accurate. In this context, the creation of formal languages plays a pivotal role, as these languages serve as tools that facilitate the representation of formal proofs. Consequently, the development and refinement of these formal languages are of paramount importance in the pursuit of sound and reliable reasoning, forming the bedrock upon which the edifice of logical thought is constructed.

This workshop will bring together theorists working on proof representations, exploiting a wide array of techniques for manifold uses, and researchers in closely related areas of application. The aim is not only to accelerate progress at the interface of theory and application, but also to identify new research directions.

The Banff International Research Station for Mathematical Innovation and Discovery (BIRS) is a collaborative Canada-US-Mexico venture that provides an environment for creative interaction as well as the exchange of ideas, knowledge, and methods within the Mathematical Sciences, with related disciplines and with industry. The research station is located at The Banff Centre in Alberta and is supported by Canada’s Natural Science and Engineering Research Council (NSERC), the U.S. National Science Foundation (NSF), and Alberta’s Advanced Education and Technology.