Jean-François Monin

Professeur à l'Université Grenoble Alpes , Polytech Grenoble; Verimag / Formal Proofs VERIMAG 150 place du torrent F-38401 Saint Martin d'Hères Tél : (+33|0) 4 57 42 22 31     Email : @univ-grenoble-alpes.fr

Plus ou moins récent

• Proof pearl: faithful computation and extraction of μ-recursive algorithms in Coq (with Dominique Larchey-Wendling, ITP 23, Byałistok, Poland, 2023) paper.
• Small inversions for smaller inversions (TYPES 22, Nantes, France, 2022) paper, Coq proofs.
• The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq (with Dominique Larchey-Wendling, book chapter, 2021) chapter.
• Developing and certifying datalog optimizations in coq/mathcomp (with Pierre Crégut and Pierre-Léo Begay, CPP, 2021) paper.
• Certican: A tool for the coq certification of CAN analysis results (with Pascal Fradet, Xiaojie Guo and Sophie Quinton, RTAS, 2019)
• Formalisation of probabilistic testing semantics in coq (with Yuxin Deng, essays dedicated to Catuscia Palamidessi, 2019) paper.
• A generic coq proof of typical worst-case analysis (with Pascal Fradet, Maxime Lesourd and Sophie Quinton, RTSS, 2018) paper.
• A generalized digraph model for expressing dependencies (with Pascal Fradet, Xiaojie Guo and Sophie Quinton, RTNS, 2018) paper.

Enseignement

• supports pour les étudiants
• Gentzen-Prawitz Natural Deduction as a Teaching Tool (with Cristian Ene and Michaël Périn, 2009) unpublished paper, also available on arxiv

Recherche

• Publications
• Présentation
• Preuves formelles
• Livre : introduction aux méthodes formelles
• Sujets de thèse
• Développements
  • otags , un générateur de tags pour emacs et vi
  • dependot , pour construire un graphe de dépendances Makefile au format dot (graphviz)
• Sujets M2R

Divers