Math Colloquium CIDMA/UAlg

Math Colloquium CIDMA/UAlg

9 November 2026

10am

• 11am

Room 3.18 of Building 2 at Gambelas Campus

FacebookInstagramTwitterEmail

Another session of the Math Seminar CIDMA/UAlg will be held, featuring speaker Simão Melo de Sousa from the University of Algarve.

When Programs Are Proofs: Type Theory, Formal Verification, Automated Reasoning, and Formalized Mathematics

Summary:

This seminar covers the fundamentals of formal verification and automated reasoning, exploring the relationship between mathematical logic, proof theory, and computer science.

Concepts such as type theory and the Curry–Howard correspondence will be presented. This establishes a connection between propositions and types, as well as between proofs and programmes, along with methods for formal verification of programmes.

The session will include examples of tools such as Rocq (formerly Coq) and Why3, used in software verification and the formalisation of mathematical results.

The challenges and opportunities associated with the use of artificial intelligence in the discovery and construction of mathematical proofs will also be discussed, weather permitting, as well as the role of formal verification in ensuring their correctness.

Cost Participation is open to the entire academic community.