Programmer = démontrer ? La correspondance de Curry-Howard aujourd'hui

Polymorphisme à tous les étages ! Du système F au calcul des constructions