Interactive Theorem Proving using Matita

Interactive theorem provers help the user to make sound mathematical proofs that are guaranteed to have no errors. They are typically used in computer science to prove critical code correct and as targets of formal methods tools. They are also used by logicians and mathematicians to organize and structure large libraries of mathematical knowledge. The seminar will gently introduce interactive theorem proving using Matita, a prover developed at the University of Bologna and closely related to Coq (France), Lean (USA) and Agda (Sweden).

Relatore

Claudio Sacerdoti Coen (Università di Bologna)

Docente di riferimento

Marco Bernardo, Giovanni Molica Bisci

Vincoli di partecipazione

Il seminario fa parte del ciclo LAAG.IT - Logica, Algebra, Analisi, Geometria e Informatica Teorica curato dai professori Marco Bernardo e Giovanni Molica Bisci. Pur raccomandando la partecipazione in presenza, il seminario si svolgerà in modalità mista simultanea tramite https://meet.google.com/smf-wxqb-mdg

Date

Luogo Data Orario Crediti (CFU)
Aula Olivetti 18 Maggio 2022 15:30-17:30 0.125