Jean-François Monin

Professor at 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

More or less recent

• 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.

Teaching

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

Research

• Publications
• Talks
• Formal proofs
• Book: Understanding Formal Methods
• PhD topics
• Developments
  • otags , a tags generator for emacs and vi
  • dependot , building a dot-graph of Makefile dependencies
• Internship topics

Miscellaneous