Seminario: “Dependent contexts and substitutions”

Martedì 13 e Martedì 20 Settembre 2016 - Per Martin-Löf


Il “visiting scientist” Professor Per Martin-Löf (Università di Stoccolma) terrà un seminario in due parti dal titolo “Dependent contexts and substitutions”.
Parte 1: Martedì 13 Settembre 2016, ore 10:00 in Aula 2AB45;
Parte 2: Martedì 20 Settembre 2016, ore 10:00 in Aula 2AB40.

Type theory will be extended with the two new forms of judgement $\Delta : ctx/\Gamma$ and $\delta : \Delta/\Gamma$, and the corresponding strengthening will be made of the notion of model of type theory in the form of category with families.

Short CV
Per Martin-Löff, member of the Royal Swedish Academy of Sciences and of the Academia Europaea, is a Swedish logician, philosopher, and mathematical statistician. He is internationally renowned for his work on the foundations of probability, statistics, mathematical logic, and computer science.
In the 1960s he gave a definition of random sequence which has remained one of the fundamental notions in probability.
He is the inventor of the notion of dependent types in the 1970s, which has strongly influenced the development of type systems at the base of many popular proof assistants for computer-aided formalization of mathematics, most notably the French Coq.
In the 1980s with G. Sambin he introduced formal topology, that is, an approach to point-free topology which can be formalized in his dependent type theory.
His type theory is also the base of the more recent work by Field medalist Vladimir Voevodsky and others on Univalent foundations for mathematics.