Simão Melo de Sousa (University of Algarve)
Formal verification and automated reasoning lie at the intersection of mathematical logic, proof theory, and computer science. Their foundations are rooted in fundamental mathematical questions concerning the nature of proofs, the formalization of reasoning, and the relationships between propositions, proofs, and mathematical constructions.
In this talk, we will revisit some of these foundations, starting with type theory and the Curry–Howard correspondence, which establishes a profound connection between propositions and types, and between proofs and programs. We will focus in particular on the role of dependent types and, time permitting, on the evolution of the notion of equality in modern formulations of type theory, including some of the ideas that led to Homotopy Type Theory.
In the second part, we will explore another perspective on formal reasoning about programs, based on program logics and deductive verification. Building on the ideas underlying Hoare logic, we will show how functional and mathematical properties of programs can be expressed through formal specifications and established with the assistance of automated reasoning systems.
These two perspectives will be illustrated using platforms such as Rocq (formerly Coq) and Why3, which combine, in different ways, specification languages, logical frameworks, and mechanisms for constructing or automating proofs. We will discuss how these tools support both software verification and the formalization and proof of mathematical results, highlighting the increasingly close relationship between certified programming and computer-assisted mathematics.
Finally, time permitting, we will discuss some of the challenges, controversies, and opportunities that artificial intelligence, particularly generative models, brings to the discovery and construction of mathematical proofs, and the fundamental role that formal verification is expected to play in ensuring their correctness.