20 février 2012
Arnaud Spiwack (Inria Paris-Rocquencourt)Je propose un petit tour d’horizon de mes travaux sur l’intéraction entre les mathématiques constructives, telles que pratiquées sur papier, et la pratique de la programmation. En particulier, je montrerai comment des systèmes de types très riches et expressifs, tels que celui de l’assistant à la démonstration Coq, rendent plus poreuse la ligne de démarcation qui sépare mathématiques et programmation.