Ciclo di seminari LAAG.IT
INTERACTIVE THEOREM PROVING USING MATITA
Nell'ambito del ciclo LAAG.IT - Logica, Algebra, Analisi, Geometria e Informatica Teorica, i professori Marco Bernardo e Giovanni Molica Bisci sono lieti di invitarvi al seminario intitolato Interactive Theorem Proving using Matita che sarà tenuto dal Prof. Claudio Sacerdoti Coen dell'Alma Mater Studiorum Università di Bologna.
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).
Il seminario si svolgerà in presenza, ma sarà anche possibile seguirlo a distanza collegandosi al link: https://meet.google.com/smf-wxqb-mdg
Data e luogo
Data inizio: 18/05/2022
alle ore 15:30
Data fine: 18/05/2022
alle ore 17:30
Collegio Raffaello (Urbino, Piazza della Repubblica, 13) Aula Olivetti
