MALINCA: focus on a few issues in logical foundations
La matematica contemporanea non è più soltanto un sistema di verità astratte, ma un campo in cui linguaggio, logica e tecnologia si intrecciano fino a ridefinire il modo stesso in cui si costruisce una dimostrazione. È in questo spazio di frontiera tra teoria e computazione che si colloca l’incontro conclusivo del ciclo “Mathematicae Lingua Franca”, dedicato al progetto europeo MALINCA e alle nuove forme della scrittura matematica.
Mercoledì 22 aprile 2026, alle ore 18:00, nell’Aula Bernardi del Collegio Ghislieri di Pavia, Hugo Herbelin (INRIA – National Institute for Research in Digital Science and Technology) terrà la conferenza dal titolo “MALINCA: focus on a few issues in logical foundations”. L’intervento approfondirà alcuni nodi cruciali emersi nel progetto MALINCA, che indaga la struttura logica e linguistica dei testi matematici e il ruolo degli assistenti di prova (proof assistants) nella formalizzazione della conoscenza.
Al centro della riflessione vi sarà il rapporto tra fondamenti logici e pratiche computazionali: come si traduce un’argomentazione matematica in un linguaggio formale? Quali sono i limiti e le potenzialità dei sistemi automatici nella verifica delle dimostrazioni? E soprattutto, come cambia la nozione stessa di “prova” quando entra in dialogo con strumenti digitali capaci di manipolare simboli e strutture logiche con precisione assoluta?
Figura di primo piano nel panorama internazionale della logica e della teoria dei tipi, Hugo Herbelin ha contribuito in modo decisivo allo sviluppo di sistemi formali per la rappresentazione delle dimostrazioni matematiche, lavorando su temi come il calcolo delle costruzioni, la logica computazionale e i linguaggi per proof assistants. La sua ricerca si colloca al crocevia tra informatica teorica, filosofia della matematica e linguistica formale, offrendo strumenti per comprendere come il pensiero matematico possa essere reso esplicito, verificabile e condivisibile anche in ambienti computazionali.
L’incontro rappresenta il momento conclusivo di un ciclo che ha messo al centro la matematica come “lingua franca” capace di attraversare discipline, tecnologie e tradizioni teoriche, aprendo una riflessione ampia sul futuro della conoscenza scientifica nell’era digitale.
Hugo Herbelin è Directeur de Recherche presso l’INRIA (Institut National de Recherche en Informatique et en Automatique), operante all'interno del laboratorio IRIF (CNRS e Université Paris Cité). È considerato uno dei massimi esperti mondiali nel campo della logica matematica, della teoria dei tipi e della corrispondenza tra prove e programmi (isomorfismo di Curry-Howard). Il suo contributo più celebre risiede nello sviluppo e nel perfezionamento di Coq, uno dei più potenti e utilizzati proof assistant (assistenti alla dimostrazione) al mondo, strumento fondamentale per la verifica formale di software critici e la formalizzazione della matematica moderna. Le sue ricerche spaziano dal calcolo delle costruzioni alla logica classica in chiave computazionale, con particolare attenzione alla semantica dei linguaggi di programmazione. L’attività di Herbelin si colloca alla frontiera tra la logica teorica e l'informatica pratica, offrendo le basi formali per garantire che sistemi complessi siano privi di errori logici e matematici.