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

Publications

Enseignement 

Ma page Google Scholar

If you don't read french and want fun,

try E, A,  C, D, R, L, G :-)

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

Toutes

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.

- DECERT, janvier 2009.

- “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).


[1] inutile de cliquer là plus d’une fois ;-)