Jean-François Monin

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

• A Minimalist Approach to Trustworthy Programming with Precise Types using Small Inversions (with Pierre Corbineau and Basile Gros, LPAR 26, Spétses, Greece, 2026) paper, slides, also at easychair.
• Proxy-based small inversions: a case study in MetaCoq programming (with Pierre Corbineau and Basile Gros, JFLA 25, Roiffé, France, 2025) paper.
• Proofs-as-programs for programmers (with Pierre Corbineau, ThEdu 24, Nancy, France, 2024) extended abstract, slides.
• 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) extended abstract, 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.

Research

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

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