Category: Évènements

Oct 31 2017

(English) Two new winter schools on Coq

Désolé, cet article est seulement disponible en Anglais Américain.

May 22 2015

(English) The Coq Workshop 2015

Désolé, cet article est seulement disponible en Anglais Américain.

Dec 19 2014

(English) First Coq Coding Sprint – June 22-25 2015 Sophia-Antipolis

Désolé, cet article est seulement disponible en Anglais Américain.

Aug 08 2014

Yves Bertot récompensé par l’ACM Software System Award

Le logiciel Coq est une nouvelle fois récompensé par l’Association for Computing Machinery. ACM Software System Award à San Francisco le 21 juin dernier prix-ACM Sur la photo, Yves Bertot (2ème sur la gauche) est entouré de quatre des huit autres récipiendaires du Software System Award 2014 :

  • Thierry Coquand, Université de Gothenburg;
  • Gérard Huet, Inria Paris – Rocquencourt;
  • Christine Paulin-Mohring, Université Paris Sud/Inria Saclay -Ile-de-France;
  • Bruno Barras, Inria Saclay/École Polytechnique;
  • Jean-Christophe Filliâtre, CNRS/Inria Saclay – Ile-de-France;
  • Hugo Herbelin, Inria Paris – Rocquencourt;
  • Chet Murthy, Google Inc.;
  • Yves Bertot, Inria Sophia Antipolis-Méditerranée ;
  • Pierre Castéran, Université de Bordeaux.

 

Apr 17 2014

(English) Coq receives the 2013 Software system Award

Désolé, cet article est seulement disponible en Anglais Américain.

Apr 05 2014

Soutenance de thèse: Interaction entre algèbre linéaire et analyse en formalisation des mathématiques

Désolé, cet article est seulement disponible en Anglais Américain.

Nov 20 2013

Soutenance de Thèse : Étude formelle d’algorithmes efficaces en algèbre linéaire

Le mercredi 20/11/2013, à partir de 13h30 à la salle de conférence I3S.

Orateur : Maxime Denès.
Titre : Étude formelle d’algorithmes efficaces en algèbre linéaire.

Résumé : Les méthodes formelles ont atteint un degré de maturité conduisant à la
conception de systèmes de preuves généralistes, permettant à la fois de
vérifier la correction de systèmes logiciels complexes ou de formaliser des
mathématiques avancées. Mais souvent, l’accent est mis davantage sur la
facilité du raisonnement sur les programmes plutôt que sur leur exécution
efficace. L’antagonisme entre ces deux aspects est particulièrement sensible
pour les algorithmes de calcul formel, dont la correction repose habituellement
sur des concepts mathématiques élaborés, mais dont l’efficacité pratique
est une préoccupation importante.
Cette thèse développe des approches à l’étude formelle et l’exécution efficace
de programmes en théorie des types, et plus précisément dans l’assistant à la
preuve Coq. Dans un premier temps, nous présentons un environnement
d’exécution permettant de compiler en code natif de tels programmes tout
en conservant la généralité et l’expressivité du formalisme.
Puis, nous nous intéressons aux représentations de données et plus
particulièrement au lien formellement vérifié et automatisé entre représentations
adaptées aux preuves ou au calcul.
Ensuite, nous mettons à profit ces techniques pour l’étude d’algorithmes
en algèbre linéaire, comme le produit matriciel de Strassen, le procédé
d’élimination de Gauss ou la mise en forme canonique de matrices, dont
notamment la forme de Smith pour les matrices sur un anneau euclidien.
Enfin, nous ouvrons le champ des applications à la formalisation et au calcul
certifié des groupes d’homologie de complexes simpliciaux issus d’images
numériques.

Mar 12 2012

MAP 2012 – International Spring School on Formalization of Mathematics

Désolé, cet article est seulement disponible en Anglais Américain.