Laurent Théry

[English]

  • Organisation: INRIA
  • Unité de Recherche: Sophia Antipolis
  • Projet: MARELLE
  • Adresse: 2004, route des Lucioles - B.P. 93 06902 Sophia Antipolis Cedex France
  • Téléphone: +33 4 92 38 76 87
  • Fax: +33 4 92 38 50 29
  • Adresse électronique: Laurent.Thery@inria.fr
  • PGP
  • Zone ftp
  • Emily, Jeremy


    Quelques Publications

    L. Fuchs, L. Théry: A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry. Automated Deduction in Geometry 2010.

    Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry
    `A Modular Formalisation of Finite Group Theory' Rapport de Recherche 6156.

    Laurent Théry et Guillaume Hanrot
    `Primality Proving with Elliptic Curves' Rapport de Recherche 6155.

    Laurent Théry,
    `Proving the group law for elliptic curves formally' Rapport Technique 330.

    Laurence Rideau et Laurent Théry,
    `Formalising Sylow's theorems in Coq', Rapport Technique 327 .

    Laurent Théry,
    ` Simplifying Polynomial Expressions in a Proof Assistant', Rapport de Recherche 5614.

    More publications

    Software

    Mon application android Morpion Mentor qui joue parfaitement au morpion.

    Mon application android Peanoware qui permet de construire des arbres de déduction naturelle.

    Des certificats de preuve pour la géometrie.

    Fourier une version par réflection de l'élimination de Fourier-Motzkin pour l'arithmetique linéaire en Coq.

    Sudoku Solver: A programme certifié qui résoud les Sudoku.

    CoqRubik: A programme certifié qui résoud le Mini Rubik.

    CoqSos un traduction du programme de somme de carrés de John Harrison pour Coq.

    CoqPrime: certifier des nombres premiers

    Logique propositionnelle: une applet pour construire des formules, une applet pour construire des arbres de preuve en déduction naturelle.

    Cyp, un outil pour colorier les preuves

    Aïoli, une boîte à outils de construction d'applications interactives.

    Figue, un moteur d'affichage bi-dimensionnel et incrémental..

    Gbcoq, une implémentation certifiée de l'algorithme de Buchberger.

    CtCaml, un environnement de programmation pour CamlLight.

    Chol, un environnement de preuve pour Hol

    Autres

    Une formalisation de la loi de groupe pour les courbes elliptiques (les courbes d'Edwards). C'est une formalisation directe d'un papier de Tom Hales.

    Une formalisation d'une généralisation des tours d'Hanoi.

    Mon exposé Devenez un champion de Moripon Fête de la Science 2016.

    Une nouvelle version de l'algorithme de Buchberger pour les bases de Gröbner dans Coq avec Ssreflect .

    Une petite animation Hopscotch in Scratch du nom de mon équipe de recherche: Marelle.

    2-Sat peut être résolu en temps linéaire

    Une preuve formelle de l'algorithme de Kosaraju

    Les décimales de Π en Coq en utilisant la formule de Plouffe

    Une preuve formelle en Coq du problème de Robbins.

    Les énigmes du Monde en Coq.

    un mini-cours virgule flottante et preuve.

    Une Preuve Formelle du théorème de Feit-Thompson (terminé le 20 Septembre 2012).

    Formalisation des algèbres géométriques.

    Résoudre le mini Rubik cube.

    Une formalisation dans l'assistant de preuve Coq d'un programme qui résoud les Sudoku: le papier et les fichiers Coq.

    Des tactiques pour manipuler des inégalités en Coq.

    Une bibliographie des mathématiques formalisées sur machine.

    Des formalisations en Coq produites par l'outil CoqDoc.

    Un cours donné sur les méthodes formelles dans une université italienne (en italien).

    Un cours donné sur Java et Esterel dans une université italienne (en italien).

    Une introduction de preuve donnée à l'ISIA en Mars 2002. Transparents (Ps, Html ou PowerPoint).

    Un exposé sur la mécanisation des preuves en arithmétique flottante donnée à l'école de printemps sur l'arithmétique des ordinateurs en Mars 2001. Transparents ou Note

    Des transparents en anglais décrivant l'intégration de l'algorithme de Stålmarck en Coq(PowerPoint,Html).

    Une formalisation de l'algorithme de Stålmarck en Coq.

    La même preuve de RSA dans différents systèmes de preuve pour l'école d'été Types 99:

    Grâce à H. Persson, une nouvelle implémentation certifiée de l'algorithme de Buchberger utilisant une preuve 100% constructive.

    Quelques exercices en Coq.


    Laurent Théry