Page personnelle de Pierre Corbineau

Coordonées

Je suis Maître de Conférences dans le groupe Systèmes Distribués et Complexes du Laboratoire VERIMAG . J'enseigne à l'école d'ingénieurs Polytech'Grenoble de l' Université Joseph Fourier .
Je suis un ancien post-doctorant dans le groupe "Fondations" du thème "Systèmes Intelligents" de l' Institut d'Informatique et de Sciences de l'Information de la Radboud Universiteit Nijmegen.
Je suis un ancien doctorant dans l'équipe Démons du Laboratoire de Recherche en Informatique

Recherche

Mes principaux sujets de recherche :

• • Preuves certifiées de sécurité de protocoles dans le modèle calculatoire
• • Création de langages de preuves plus adaptés pour les mathématiciens
  • Création d'interfaces collaboratives de preuve formelle interactiuve en ligne
• • Recherche de preuves en logique intuitionniste du premier ordre
  • Recherche de preuves équationnelles
  • Représentation et vérification de preuves en théorie des types

Vous pouvez consulter la liste de mes publications.

Enseignement

Je suis enseignant titulaire à Polytech'Grenoble dans le cycle ingénieur, à la fois dans le cursus classique et celui par alternance (départments 3I et E2I). Je suis le responsable pédagogique de l'année 3 de 3I.

• Microcontrôleurs (3I,3)
• Programmation Orientée-objet (E2I,4)

• Projet systèmes embarqués (3I,3)
• Algorithmique et Programmation (E2I,3)
• Programmation système UNIX (E2I,5)

En 2010-2011, j'ai également enseigné la partie Logique de l'option Informatique pour la préparation à l'Agrégation de Mathématiques.

Programmation

• C-zar : le Langage déclaratif de preuve pour Coq : ici.
• Un vérificateur de types / évaluateur d'expressions pour les systèmes de types purs : ici.
• Une implantation en Objective Caml d'arbres binaires aléatoires :
ici
• Preuves du premier ordre par réflexion en Coq : v8.0pl3 / SVN
• Contributions à l'assistant de preuve Coq