Loïc Pottier chargé de recherche, HDR INRIA Sophia Antipolis Méditerrannée, équipe Marelle loic.pottier@sophia.inria.fr Tel: 04 92 38 78 19 / 06 61 25 61 92 If you don't read french and want fun, Pour venir au travail, j’utilise ça . |
|
Je m'intéresse actuellement à la mécanisation des preuves mathématiques. Ma page web la plus récente est ici.[1]
Récemment:
février 2012: début du cours de logique en MAM3 de Polytech’Nice. La page du cours est ici.
novembre 2011: les transparents du cours “Preuves formelles automatiques en géométrie” aux JNCF 2011: partie 1, partie 2. Démo. Le cours est publié ici par le CIRM.
août 2011: voici les tactiques nsatz, cring et non_commutative_ring reprises en utilisant au maximum les classes de types: nsatz-8.3pl2.tgz, setoid_ring-8.3pl2.tgz.
On peut facilement les utiliser avec Ssreflect, voici un exemple avec des matrices.
avril 2011: en reprenant du vieux code sur les téléscopes, voilà un début de généralisation des structures algébriques utilisant les classes de types.
décembre 2010: étude et simplification de la preuve d'extentionnalité de V.Voevodsky.
Publications
La dernière: Proof certificates for algebra and their application to automatic geometry theorem proving Benjamin Grégoire, Loïc Pottier, Laurent Théry, LNAI, vol 6301, 2011
Exposés
- Journées Nationales de Calcul Formel, novembre 2011:
mini-cours de 3h “Preuves formelles automatiques en géométrie” (cours et transparents: 1, 2), démo de Coq.
- groupe de travail Coq sur la réification, voilà mes transparents.
Enseignement
Cette année, comme les deux années passées, de février à mai je donne un cours de logique niveau L3 à Polytech'Nice. Les TD sont faits en Coq.
Depuis quelques années, je m'occupais d'un groupe de TD de sémantique en M1 informatique à l'université de Nice (le cours est fait par Yves Bertot). Avant j'y faisais un cours de lambda-calcul.
En 2003-2006, j'avais donné un cours sur les preuves formelles en DEA/M2 de mathématiques à Nice.
De 1991 à 2001, j'assurais un cours de logique en maîtrise de mathématiques à l'université de Nice, qui s'était orienté d'année en année vers le lambda-calcul et les preuves formelles en Coq.