construcivisme et multiplications

G.Allais - Multiplications

Presentation

Je suis élève de l’ENS Lyon en M2 au Master parisien de recherche en informatique (MPRI). Je suis en ce moment en stage de 5 mois au sein du Computational Logic Group de l’université d’Innsbruck où je travaille sur la certification de preuves de terminaison (en contribuant à CeTA)

Sujets de prédilection

Je m’intéresse particulièrement à la logique (constructiviste) et à sa relation avec la notion de calcul des multiplications. Cela passe bien entendu par la théorie des types (dépendants) pour la logique (que ce soit au tableau ou via un assistant de preuve tel que Coq) et pour le calcul (avec un langage de programmation équipé de types dépendants tel qu’Agda)

Actualités

L’équipe Coqtail a 3 présentations acceptées cet été ! Nous discuterons de la formalisation des séries entières en Coq au workshop THedu’11 (Cade23, Wroclaw, Pologne) et d’une axiomatique alternative pour ℝ ainsi que de l’utilisation de la reflection pour resoudre des équations différentielles au 3° Workshop Coq (ITP 2011, Nimègue, Hollande).

Tables de multiplication : apprentissage