Marius travaille sur l'assistant de preuve Coq. Il ne nous en parlera pas (cette année!). En attendant, une petite introduction au langage catégorique, un jeu avec les F-algèbres et c'est parti pour généraliser la notion d'induction !

Si jamais tu n'as pas pu assister à la conférence ou bien si un détail te chiffonne, n'hésite pas à aller voir le compte rendu de la conférence.