Jean-François Monin

According to our database, Jean-François Monin authored at least 31 papers between 1984 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq.

Dominique Larchey-Wendling, Jean-François Monin

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2021

Developing and certifying Datalog optimizations in coq/mathcomp.

Pierre-Léo Bégay, Pierre Crégut, Jean-François Monin

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2019

CertiCAN: A Tool for the Coq Certification of CAN Analysis Results.

Pascal Fradet, Xiaojie Guo, Jean-François Monin, Sophie Quinton

Proceedings of the 25th IEEE Real-Time and Embedded Technology and Applications Symposium, 2019

Formalisation of Probabilistic Testing Semantics in Coq.

Yuxin Deng, Jean-François Monin

Proceedings of the Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy, 2019

2018

A Generic Coq Proof of Typical Worst-Case Analysis.

Pascal Fradet, Maxime Lesourd, Jean-François Monin, Sophie Quinton

Proceedings of the 2018 IEEE Real-Time Systems Symposium, 2018

A Generalized Digraph Model for Expressing Dependencies.

Pascal Fradet, Xiaojie Guo, Jean-François Monin, Sophie Quinton

Proceedings of the 26th International Conference on Real-Time Networks and Systems, 2018

2017

Work-in-Progress: Toward a Coq-Certified Tool for the Schedulability Analysis of Tasks with Offsets.

Xiaojie Guo, Sophie Quinton, Pascal Fradet, Jean-François Monin

Proceedings of the 2017 IEEE Real-Time Systems Symposium, 2017

2015

Towards Verified Faithful Simulation.

Vania Joloboff, Jean-François Monin, Xiaomu Shi

Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2015

2013

Handcrafted Inversions Made Operational on Operational Semantics.

Jean-François Monin, Xiaomu Shi

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012

Formal Verification of Netlog Protocols.

Meixian Chen, Jean-François Monin

Proceedings of the Sixth International Symposium on Theoretical Aspects of Software Engineering, 2012

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

A Framework for Verifying Data-Centric Protocols.

Yuxin Deng, Stéphane Grumbach, Jean-François Monin

Proceedings of the Formal Techniques for Distributed Systems, 2011

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

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2009

Gentzen-Prawitz Natural Deduction as a Teaching Tool

Jean-François Monin, Cristian Ene, Michaël Périn

CoRR, 2009

Verifying Self-stabilizing Population Protocols with Coq.

Yuxin Deng, Jean-François Monin

Proceedings of the TASE 2009, 2009

2006

Proving termination using dependent types: the case of XOR-terms.

Jean-François Monin, Judicaël Courant

Proceedings of the Revised Selected Papers from the Seventh Symposium on Trends in Functional Programming, 2006

2004

Proof Pearl: From Concrete to Functional Unparsing.

Jean-François Monin

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

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

Understanding formal methods.

Jean-François Monin

Springer, ISBN: 978-1-85233-247-1, 2003

2000

Proving the Correctness of the Standardized Algorithm for ABR Conformance.

Jean-François Monin

Formal Methods Syst. Des., 2000

1999

Correctness Proof of the Standardized Algorithm for ABR Conformance.

Jean-François Monin, Francis Klay

Proceedings of the FM'99 - Formal Methods, 1999

1996

Exceptions Considered Harmless.

Jean-François Monin

Sci. Comput. Program., 1996

Proving a Real Time Algorithm for ATM in Coq.

Jean-François Monin

Proceedings of the Types for Proofs and Programs, 1996

1995

Extracting Programs with Exceptions in an Impredicative Type System.

Jean-François Monin

Proceedings of the Mathematics of Program Construction, 1995

1993

The Parallel Abstract Machine: A Common Execution Model for FDTs.

Guillaume Doumenc, Jean-François Monin

Proceedings of the FME '93: Industrial-Strength Formal Methods, 1993

1991

Real-size Compiler Writing Using Prolog with Arrows.

Jean-François Monin

Proceedings of the Logic Programming, 1991

1988

Development of Véda, a Prototyping Tool for Distributed Algorithms.

Claude Jard, Jean-François Monin, Roland Groz

IEEE Trans. Software Eng., 1988

A Compiler Written in Prolog: The Véda Experience.

Jean-François Monin

Proceedings of the Programming Language Implementation and Logic Programming, 1988

1987

Est-ce que Prolog sait lire?

Jean-François Monin, E. Barrielle

Proceedings of the SPLT'87, 1987

1985

Experience in implementing ESTELLE-X.250 (a CCITT subset of ESTELLE) in VEDA.

Claude Jard, Jean-François Monin, Roland Groz

Proceedings of the Protocol Specification, 1985

1984

Ecriture d'un compilateur "réel" en PROLOG.

Jean-François Monin

Proceedings of the SPLT'84, 1984