Jean-François Monin

Publication Activity (10 Years)

Years Active: 1984-2023
Publications (10 Years): 8

Top Topics

Formal Semantics

Worst Case Analysis

Operational Semantics

Top Venues

Publications

Dominique Larchey-Wendling, Jean-François Monin
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. ITP (2023)
Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin
Developing and certifying Datalog optimizations in coq/mathcomp. CPP (2021)
Yuxin Deng, Jean-François Monin
Formalisation of Probabilistic Testing Semantics in Coq. The Art of Modelling Computational Systems (2019)
Pascal Fradet, Xiaojie Guo, Jean-François Monin, Sophie Quinton
CertiCAN: A Tool for the Coq Certification of CAN Analysis Results. RTAS (2019)
Pascal Fradet, Maxime Lesourd, Jean-François Monin, Sophie Quinton
A Generic Coq Proof of Typical Worst-Case Analysis. RTSS (2018)
Pascal Fradet, Xiaojie Guo, Jean-François Monin, Sophie Quinton
A Generalized Digraph Model for Expressing Dependencies. RTNS (2018)
Xiaojie Guo, Sophie Quinton, Pascal Fradet, Jean-François Monin
Work-in-Progress: Toward a Coq-Certified Tool for the Schedulability Analysis of Tasks with Offsets. RTSS (2017)
Vania Joloboff, Jean-François Monin, Xiaomu Shi
Towards Verified Faithful Simulation. SETTA (2015)
Jean-François Monin, Xiaomu Shi
Handcrafted Inversions Made Operational on Operational Semantics. ITP (2013)
Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui
First steps towards the certification of an ARM simulator using Compcert CoRR (2012)
Meixian Chen, Jean-François Monin
Formal Verification of Netlog Protocols. TASE (2012)
Frédéric Blanqui, Claude Helmstetter, Vania Joloboff, Jean-François Monin, Xiaomu Shi
Designing a CPU model: from a pseudo-formal document to fast code CoRR (2011)
Yuxin Deng, Stéphane Grumbach, Jean-François Monin
A Framework for Verifying Data-Centric Protocols. FMOODS/FORTE (2011)
Xiaomu Shi, Jean-François Monin, Frédéric Tuong, Frédéric Blanqui
First Steps towards the Certification of an ARM Simulator Using Compcert. CPP (2011)
Jean-François Monin, Cristian Ene, Michaël Périn
Gentzen-Prawitz Natural Deduction as a Teaching Tool CoRR (2009)
Yuxin Deng, Jean-François Monin
Verifying Self-stabilizing Population Protocols with Coq. TASE (2009)
Jean-François Monin, Judicaël Courant
Proving termination using dependent types: the case of XOR-terms. Trends in Functional Programming (2006)
Jean-François Monin
Proof Pearl: From Concrete to Functional Unparsing. TPHOLs (2004)
Béatrice Bérard, Laurent Fribourg, Francis Klay, Jean-François Monin
Compared Study of Two Correctness Proofs for the Standardized. Formal Methods Syst. Des. 22 (1) (2003)
Jean-François Monin
Proving the Correctness of the Standardized Algorithm for ABR Conformance. Formal Methods Syst. Des. 17 (3) (2000)
Jean-François Monin, Francis Klay
Correctness Proof of the Standardized Algorithm for ABR Conformance. World Congress on Formal Methods (1999)
Jean-François Monin
Proving a Real Time Algorithm for ATM in Coq. TYPES (1996)
Jean-François Monin
Exceptions Considered Harmless. Sci. Comput. Program. 26 (1-3) (1996)
Jean-François Monin
Extracting Programs with Exceptions in an Impredicative Type System. MPC (1995)
Guillaume Doumenc, Jean-François Monin
The Parallel Abstract Machine: A Common Execution Model for FDTs. FME (1993)
Jean-François Monin
Real-size Compiler Writing Using Prolog with Arrows. ICLP (1991)
Claude Jard, Jean-François Monin, Roland Groz
Development of Véda, a Prototyping Tool for Distributed Algorithms. IEEE Trans. Software Eng. 14 (3) (1988)
Jean-François Monin
A Compiler Written in Prolog: The Véda Experience. PLILP (1988)
Jean-François Monin, E. Barrielle
Est-ce que Prolog sait lire? SPLT (1987)
Claude Jard, Jean-François Monin, Roland Groz
Experience in implementing ESTELLE-X.250 (a CCITT subset of ESTELLE) in VEDA. PSTV (1985)
Jean-François Monin
Ecriture d'un compilateur "réel" en PROLOG. SPLT (1984)