Jean-François Monin

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

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

On csauthors.net:

Bibliography

2023
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq.
Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2021
Developing and certifying Datalog optimizations in coq/mathcomp.
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.
Proceedings of the 25th IEEE Real-Time and Embedded Technology and Applications Symposium, 2019

Formalisation of Probabilistic Testing Semantics in Coq.
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.
Proceedings of the 2018 IEEE Real-Time Systems Symposium, 2018

A Generalized Digraph Model for Expressing Dependencies.
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.
Proceedings of the 2017 IEEE Real-Time Systems Symposium, 2017

2015
Towards Verified Faithful Simulation.
Proceedings of the Dependable Software Engineering: Theories, Tools, and Applications, 2015

2013
Handcrafted Inversions Made Operational on Operational Semantics.
Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2012
Formal Verification of Netlog Protocols.
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
CoRR, 2011

A Framework for Verifying Data-Centric Protocols.
Proceedings of the Formal Techniques for Distributed Systems, 2011

First Steps towards the Certification of an ARM Simulator Using Compcert.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2009
Gentzen-Prawitz Natural Deduction as a Teaching Tool
CoRR, 2009

Verifying Self-stabilizing Population Protocols with Coq.
Proceedings of the TASE 2009, 2009

2006
Proving termination using dependent types: the case of XOR-terms.
Proceedings of the Revised Selected Papers from the Seventh Symposium on Trends in Functional Programming, 2006

2004
Proof Pearl: From Concrete to Functional Unparsing.
Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

2003
Compared Study of Two Correctness Proofs for the Standardized.
Formal Methods Syst. Des., 2003

Understanding formal methods.
Springer, ISBN: 978-1-85233-247-1, 2003

2000
Proving the Correctness of the Standardized Algorithm for ABR Conformance.
Formal Methods Syst. Des., 2000

1999
Correctness Proof of the Standardized Algorithm for ABR Conformance.
Proceedings of the FM'99 - Formal Methods, 1999

1996
Exceptions Considered Harmless.
Sci. Comput. Program., 1996

Proving a Real Time Algorithm for ATM in Coq.
Proceedings of the Types for Proofs and Programs, 1996

1995
Extracting Programs with Exceptions in an Impredicative Type System.
Proceedings of the Mathematics of Program Construction, 1995

1993
The Parallel Abstract Machine: A Common Execution Model for FDTs.
Proceedings of the FME '93: Industrial-Strength Formal Methods, 1993

1991
Real-size Compiler Writing Using Prolog with Arrows.
Proceedings of the Logic Programming, 1991

1988
Development of Véda, a Prototyping Tool for Distributed Algorithms.
IEEE Trans. Software Eng., 1988

A Compiler Written in Prolog: The Véda Experience.
Proceedings of the Programming Language Implementation and Logic Programming, 1988

1987
Est-ce que Prolog sait lire?
Proceedings of the SPLT'87, 1987

1985
Experience in implementing ESTELLE-X.250 (a CCITT subset of ESTELLE) in VEDA.
Proceedings of the Protocol Specification, 1985

1984
Ecriture d'un compilateur "réel" en PROLOG.
Proceedings of the SPLT'84, 1984


  Loading...