Math Colloquium CIDMA/UAlg

Realiza-se mais uma sessão do Math Seminar CIDMA/UAlg, que terá como orador Simão Melo de Sousa, da Universidade do Algarve.

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

Resumo:

Este seminário aborda os fundamentos da verificação formal e do raciocínio automatizado, explorando a relação entre lógica matemática, teoria das demonstrações e informática. 

Serão apresentados conceitos como a teoria dos tipos, a correspondência de Curry–Howard, que estabelece uma ligação entre proposições e tipos, e entre demonstrações e programas, bem como métodos de verificação formal de programas.

A sessão incluirá exemplos de ferramentas como Rocq (anteriormente Coq) e Why3, utilizadas na verificação de software e na formalização de resultados matemáticos. 

Serão ainda discutidos, caso o tempo o permita, os desafios e as oportunidades associados à utilização da inteligência artificial na descoberta e construção de demonstrações matemáticas, bem como o papel da verificação formal na garantia da sua correção.