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; autrement aussi. |
|
Depuis le 4 septembre, et pour l’année 2012-2013, je suis détaché dans l’Éducation nationale et j’enseigne les mathématiques en classe préparatoire. Ça me prend tout mon temps et c’est passionnant! |
Ma page web la plus récente est ici.[1]
Avant, je m’intéressais principalement à la mécanisation des preuves mathématiques.
Récemment:
mai 2012: fin du cours de logique. J’ai réécrit mes notes de cours avec Texmacs, puis les ai converties en Latex, avec la police Garamond de Claude Garamont. C’est ici.
février 2012: début du cours de logique en MAM3 de Polytech’Nice (70h). 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 récents
- 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, mars 2011, voilà mes transparents.
- “Au coeur des flèches”, conférence à l’IREM de Nice, journée sur les démonstrations mathématiques, juin 2007.
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 très souvent 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. Quelques années auparavant, j’avais donné un cours de DEA de mathématiques à Nice sur la résolution de systèmes polynomiaux creux.
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.
Avant, j’ai enseigné des mathématiques (DEUG, Lycée), de l’informatique (compilation, algorithmique, Lisp, Prolog, Maple, Pascal).