Ecriture d'un compilateur "réel" en PROLOG. - Jean-François Monin (SPLT, 1984)

Experience in implementing ESTELLE-X.250 (a CCITT subset of ESTELLE) in VEDA. - Claude Jard; Jean-François Monin; Roland Groz (PSTV, 1985)

Est-ce que Prolog sait lire? - Jean-François Monin; E. Barrielle (SPLT, 1987)

A Compiler Written in Prolog: The Véda Experience. - Jean-François Monin (PLILP, 1988)

Development of Véda, a Prototyping Tool for Distributed Algorithms. - Claude Jard; Jean-François Monin; Roland Groz (IEEE Trans. Software Eng., 1988)

Real-size Compiler Writing Using Prolog with Arrows. - Jean-François Monin (ICLP, 1991)

The Parallel Abstract Machine: A Common Execution Model for FDTs. - Guillaume Doumenc; Jean-François Monin (FME, 1993)

Extracting Programs with Exceptions in an Impredicative Type System. - Jean-François Monin (MPC, 1995)

Proving a Real Time Algorithm for ATM in Coq. - Jean-François Monin (TYPES, 1996)

Exceptions Considered Harmless. - Jean-François Monin (Sci. Comput. Program., 1996)

Correctness Proof of the Standardized Algorithm for ABR Conformance. - Jean-François Monin; Francis Klay (World Congress on Formal Methods, 1999)

Proving the Correctness of the Standardized Algorithm for ABR Conformance. - Jean-François Monin (Formal Methods Syst. Des., 2000)

Understanding formal methods. - Jean-François Monin (Springer, 2003)

Compared Study of Two Correctness Proofs for the Standardized. - Béatrice Bérard; Laurent Fribourg; Francis Klay; Jean-François Monin (Formal Methods Syst. Des., 2003)

Proof Pearl: From Concrete to Functional Unparsing. - Jean-François Monin (TPHOLs, 2004)

Proving termination using dependent types: the case of XOR-terms. - Jean-François Monin; Judicaël Courant (Trends in Functional Programming, 2006)

Verifying Self-stabilizing Population Protocols with Coq. - Yuxin Deng; Jean-François Monin (TASE, 2009)

Gentzen-Prawitz Natural Deduction as a Teaching Tool - Jean-François Monin; Cristian Ene; Michaël Périn (CoRR, 2009)

First Steps towards the Certification of an ARM Simulator Using Compcert. - Xiaomu Shi; Jean-François Monin; Frédéric Tuong; Frédéric Blanqui (CPP, 2011)

A Framework for Verifying Data-Centric Protocols. - Yuxin Deng; Stéphane Grumbach; Jean-François Monin (FMOODS/FORTE, 2011)

Designing a CPU model: from a pseudo-formal document to fast code - Frédéric Blanqui; Claude Helmstetter; Vania Joloboff; Jean-François Monin; Xiaomu Shi (CoRR, 2011)

Formal Verification of Netlog Protocols. - Meixian Chen; Jean-François Monin (TASE, 2012)

Handcrafted Inversions Made Operational on Operational Semantics. - Jean-François Monin; Xiaomu Shi (ITP, 2013)

Towards Verified Faithful Simulation. - Vania Joloboff; Jean-François Monin; Xiaomu Shi (SETTA, 2015)

Work-in-Progress: Toward a Coq-Certified Tool for the Schedulability Analysis of Tasks with Offsets. - Xiaojie Guo 003; Sophie Quinton; Pascal Fradet; Jean-François Monin (RTSS, 2017)

A Generalized Digraph Model for Expressing Dependencies. - Pascal Fradet; Xiaojie Guo 003; Jean-François Monin; Sophie Quinton (RTNS, 2018)

A Generic Coq Proof of Typical Worst-Case Analysis. - Pascal Fradet; Maxime Lesourd; Jean-François Monin; Sophie Quinton (RTSS, 2018)

Formalisation of Probabilistic Testing Semantics in Coq. - Yuxin Deng; Jean-François Monin (The Art of Modelling Computational Systems, 2019)

CertiCAN: A Tool for the Coq Certification of CAN Analysis Results. - Pascal Fradet; Xiaojie Guo 003; Jean-François Monin; Sophie Quinton (RTAS, 2019)

Developing and certifying Datalog optimizations in coq/mathcomp. - Pierre-Léo Bégay; Pierre Crégut; Jean-François Monin (CPP, 2021)

Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. - Dominique Larchey-Wendling; Jean-François Monin (ITP, 2023)