Coq : aspects pratiques de la théorie des types

Algorithmes, machines et langages – Yves Bertot (Inria Sophia-Antipolis) et Pierre Castéran (Labri, Laboratoire Bordelais de Recherche en Informatique )

www.college-de-france.fr/site/gerard-berry/seminar-2018-12-13-17h30.htm