@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: bib2bib -oc simpl_index.bib.liste -ob simpl_index.bib --remove abstract --remove pdf --remove ps index.bib}}
@inproceedings{itp23-murec,
author = {Larchey-Wendling, Dominique and Monin, Jean-Fran\c{c}ois},
title = {{Proof Pearl: Faithful Computation and Extraction of \mu-Recursive Algorithms in Coq}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {21:1--21:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
isbn = {978-3-95977-284-6},
issn = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
url = {https://drops.dagstuhl.de/opus/volltexte/2023/18396},
urn = {urn:nbn:de:0030-drops-183963},
doi = {10.4230/LIPIcs.ITP.2023.21},
annote = {Keywords: Unbounded linear search, \mu-recursive functions, computational contents, Coq, extraction, OCaml}
}
@inproceedings{types22-smallinv,
author = {Jean{-}Fran{\c{c}}ois Monin},
title = {Small inversions for smaller inversions},
booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022 Abstracts)},
year = 2022,
editor = {Delia Kesner and Pierre-Marie P\'edrot},
month = {June},
address = {Nantes}
}
@inbook{braga21,
author = {Dominique Larchey{-}Wendling and Jean{-}Fran{\c{c}}ois Monin},
editor = {Klaus Mainzer and Peter Schuster and Helmut Schwichtenberg},
chapter = 8,
title = {{The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq}},
booktitle = {Proof and Computation II: From Proof Theory and Univalent Mathematics to Program Extraction and Verification},
publisher = {World Scientific},
year = 2021,
crossref = {proof-comput-II},
month = {September},
pages = {305--386}
}
@book{proof-comput-II,
editor = {Klaus Mainzer and Peter Schuster and Helmut Schwichtenberg},
title = {Proof and Computation II: From Proof Theory and Univalent Mathematics to Program Extraction and Verification},
publisher = {World Scientific},
year = 2021,
month = {September}
}
@inproceedings{datalog-cpp21,
author = {Pierre-L{\'e}o Begay and Pierre Cr{\'e}gut and
Jean{-}Fran{\c{c}}ois Monin},
title = {Developing and certifying Datalog optimizations in Coq/MathComp},
booktitle = {10th ACM SIGPLAN International Conference on Certified Proofs and Programs},
year = 2021,
editor = {Catalin Hritcu and Andrei Popescu}
}
@inproceedings{catuscia19-probatesting,
author = {Yuxin Deng and
Jean{-}Fran{\c{c}}ois Monin},
title = {Formalisation of Probabilistic Testing Semantics in Coq},
booktitle = {The Art of Modelling Computational Systems: {A} Journey from Logic
and Concurrency to Security and Privacy - Essays Dedicated to Catuscia
Palamidessi on the Occasion of Her 60th Birthday},
pages = {276--292},
year = {2019},
editor = {M{\'{a}}rio S. Alvim and
Kostas Chatzikokolakis and
Carlos Olarte and
Frank Valencia},
series = {Lecture Notes in Computer Science},
volume = {11760},
publisher = {Springer},
timestamp = {Thu, 07 Nov 2019 17:02:36 +0100},
biburl = {https://dblp.org/rec/bib/conf/birthday/DengM19},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{rtas19-certican,
author = {Pascal Fradet and
Xiaojie Guo and
Jean{-}Fran{\c{c}}ois Monin and
Sophie Quinton},
title = {CertiCAN: {A} Tool for the Coq Certification of {CAN} Analysis Results},
booktitle = {25th {IEEE} Real-Time and Embedded Technology and Applications Symposium,
{RTAS} 2019, Montreal, QC, Canada, April 16-18, 2019},
pages = {182--191},
year = {2019},
editor = {Bj{\"{o}}rn B. Brandenburg},
publisher = {{IEEE}},
timestamp = {Wed, 16 Oct 2019 14:14:55 +0200},
biburl = {https://dblp.org/rec/bib/conf/rtas/FradetGMQ19},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{rtns18-digraphs,
author = {Pascal Fradet and
Xiaojie Guo and
Jean{-}Fran{\c{c}}ois Monin and
Sophie Quinton},
title = {A Generalized Digraph Model for Expressing Dependencies},
booktitle = {Proceedings of the 26th International Conference on Real-Time Networks
and Systems, {RTNS} 2018, Chasseneuil-du-Poitou, France, October 10-12,
2018},
pages = {72--82},
year = {2018},
editor = {Yassine Ouhammou and
Fr{\'{e}}d{\'{e}}ric Ridouard and
Emmanuel Grolleau and
Mathieu Jan and
Moris Behnam},
publisher = {{ACM}},
timestamp = {Wed, 21 Nov 2018 12:44:19 +0100},
biburl = {https://dblp.org/rec/bib/conf/rtns/FradetGMQ18},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@inproceedings{types18-indrec,
author = {Dominique Larchey-Wendling and Jean{-}Fran{\c{c}}ois Monin},
title = {Simulating induction-recursion for partial algorithms},
booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018 Abstracts)},
year = 2018,
editor = {Jos\`{e} Esp\`{i}rito Santo and Lu\`{i}s Pinto},
month = {June},
address = {Braga}
}
@inproceedings{rtss18-typical,
author = {Pascal Fradet and
Maxime Lesourd and
Jean{-}Fran{\c{c}}ois Monin and
Sophie Quinton},
title = {A Generic Coq Proof of Typical Worst-Case Analysis},
booktitle = {2018 {IEEE} Real-Time Systems Symposium, {RTSS} 2018, Nashville, TN,
USA, December 11-14, 2018},
pages = {218--229},
year = {2018},
title = {2018 {IEEE} Real-Time Systems Symposium, {RTSS} 2018, Nashville, TN,
USA, December 11-14, 2018},
publisher = {{IEEE} Computer Society},
isbn = {978-1-5386-7908-1},
timestamp = {Wed, 16 Oct 2019 14:14:53 +0200}
}
@inproceedings{rtss17-offsets,
author = {Xiaojie Guo and
Sophie Quinton and
Pascal Fradet and
Jean{-}Fran{\c{c}}ois Monin},
title = {Work-in-Progress: Toward a Coq-Certified Tool for the Schedulability
Analysis of Tasks with Offsets},
booktitle = {2017 {IEEE} Real-Time Systems Symposium, {RTSS} 2017, Paris, France,
December 5-8, 2017},
publisher = {{IEEE} Computer Society},
pages = {387--389},
year = {2017},
timestamp = {Wed, 16 Oct 2019 14:14:53 +0200},
biburl = {https://dblp.org/rec/bib/conf/rtss/GuoQFM17},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@incollection{mifi17,
author = {Joloboff, Vania and Monin, Jean-Fran\c{c}ois and Shi, Xiaomu},
title = {{SimSoC: A Fast, Proven Faithful, Full System Virtual Prototyping Framework}},
year = {2017},
booktitle = {{Model-Implementation Fidelity in Cyber Physical System Design}},
editor = {Anca Molnos and Christian Fabre},
pages = {129--156},
publisher = {Springer}
}
@inproceedings{setta15,
author = {Vania Joloboff and
Jean-Fran\c{c}ois Monin and
Xiaomu Shi},
title = {{Towards Verified Faithful Simulation}},
booktitle = {Dependable Software Engineering: Theories, Tools, and Applications
- First International Symposium, {SETTA} 2015, Nanjing, China, November
4-6, 2015, Proceedings},
pages = {105--119},
year = {2015},
editor = {Xuandong Li and
Zhiming Liu and
Wang Yi},
series = {Lecture Notes in Computer Science},
volume = {9409},
publisher = {Springer}
}
@inproceedings{itp13,
author = {Jean-Fran\c{c}ois Monin and Xiaomu Shi},
title = {{Handcrafted Inversions Made Operational on Operational Semantics}},
booktitle = {ITP 2013},
pages = {338-353},
year = 2013,
editor = {Blazy, S. and Paulin, C. and Pichardie, D.},
volume = 7998,
series = {LNCS},
address = {Rennes, France},
month = {July},
publisher = {Springer}
}
@inproceedings{tase12,
author = {Meixian Chen and
Jean-Fran\c{c}ois Monin},
title = {{Formal Verification of Netlog Protocols}},
editor = {Tiziana Margaria and
Zongyan Qiu and
Hongli Yang},
booktitle = {Sixth International Symposium on Theoretical Aspects of
Software Engineering, TASE 2012, 4-6 July 2012, Beijing,
China},
publisher = {IEEE},
isbn = {978-0-7695-4751-0},
year = {2012},
pages = {43-50}
}
@inproceedings{cpp11,
author = {Xiaomu Shi and
Jean-Fran\c{c}ois Monin and
Fr\'ed\'eric Tuong and
Fr\'ed\'eric Blanqui},
title = {{First Steps towards the Certification of an ARM Simulator
Using Compcert}},
booktitle = {Certified Proofs and Programs - First International Conference},
year = {2011},
month = {December 7-9},
address = {Kenting, Taiwan},
pages = {346-361},
editor = {Jean-Pierre Jouannaud and Zhong Shao},
publisher = {Springer},
series = {LNCS},
volume = {7086},
isbn = {978-3-642-25378-2}
}
@inproceedings{discotec11,
author = {Yuxin Deng and St\'ephane Grumbach and Jean-Fran\c{c}ois Monin},
title = {{A Framework for Verifying Data-Centric Protocols}},
booktitle = {FMOODS/FORTE 2011},
address = {Reykjavik, Iceland},
year = 2011,
editor = {Bruni, R. and Dingel, J.},
volume = {6722},
pages = {106-120},
series = {LNCS},
month = {June 6-9},
publisher = {Springer}
}
@techreport{bfs-RR-Inria11,
author = {Yuxin Deng and St\'{e}phane Grumbach and Jean-Fran\c{c}ois Monin},
title = {{Verifying Declarative Netlog Protocols with Coq: a First Experiment}},
institution = {INRIA},
year = 2011,
type = {Research Report},
pages = {25},
number = 7511
}
@inproceedings{rapido11,
author = {Blanqui, Fr\'ed\'eric and Helmstetter, Claude and
Joloboff, Vania and Monin, Jean-Fran\c{c}ois and Shi, Xiaomu},
title = {Designing a {CPU} model: from a pseudo-formal document to
fast code},
booktitle = {Proceedings of the 3rd Workshop on
Rapid Simulation and Performance Evaluation: Methods and Tools},
address = {Heraklion, Greece},
month = {January},
year = 2011,
note = {Best Paper Award}
}
@inproceedings{monin10_inversion,
hal_id = {inria-00489412},
url = {https://hal.inria.fr/inria-00489412/en/},
title = { {P}roof {T}rick: {S}mall {I}nversions},
author = {{M}onin, {J}ean-{F}ran{\c{c}}ois},
language = {{A}nglais},
affiliation = {{FORMES} - {LIAMA} - {INRIA} - {T}singhua
{U}niversity / {B}eijing - {LIAMA} -
{U}niversit\'e {J}oseph {F}ourier - {UJF} -
{U}niversit\'e {J}oseph {F}ourier - {G}renoble {I}
},
booktitle = {{S}econd {C}oq {W}orkshop },
address = {{E}dinburgh {R}oyaume-{U}ni },
editor = {{Y}ves {B}ertot },
audience = {internationale },
day = {09},
month = {July},
year = {2010}
}
@misc{simsoc_cert10,
author = {Blanqui, F. AND Helmstetter, C. AND Joloboff, V. AND Monin, J.-F. AND Shi, X.},
title = {{SimSoC-Cert: a Certified Simulator for Systems on Chip}},
howpublished = {Draft},
month = {September},
year = {2010}
}
@misc{coqnetlog_RR,
title = {{Towards Verifying Declarative Netlog Protocols with Coq}},
author = {Deng, Yuxin AND Grumbach, Stephane AND Monin, Jean-Fran\c{c}ois},
howpublished = {Draft},
pages = {20},
month = {June},
year = {2010},
url = {https://hal.inria.fr/inria-00506093/en/}
}
@inproceedings{dengmonin09tase,
author = {Yuxin Deng and Jean-Fran\c{c}ois Monin},
title = {{Verifying self-stabilizing population protocols with Coq}},
booktitle = {3rd IEEE International Symposium on Theoretical Aspects of Software Engineering},
year = 2009,
editor = {Jifeng HE and Michael Hinchey and Xirong Ma},
address = {Tianjin, China},
month = {July}
}
@article{gpnd09,
author = {Jean-Fran\c{c}ois Monin and
Cristian Ene and
Micha\"el P\'erin},
title = {Gentzen-Prawitz Natural Deduction as a Teaching Tool},
journal = {CoRR},
volume = {abs/0907.3599},
year = {2009},
ee = {https://arxiv.org/abs/0907.3599},
bibsource = {DBLP, https://dblp.uni-trier.de}
}
@incollection{monin08_universalis,
author = {Jean-Fran\c{c}ois Monin},
title = {Programmation},
howpublished = {Encyclop{\ae}dia Universalis, Corpus},
year = 2008
}
@unpublished{CML06:_balwords,
author = {Judica{\"e}l Courant and Jean-Fran\c{c}ois Monin and Yassine Lakhnech},
title = {Proof pearl: elementary inductive and integer-based
proofs about balanced words},
note = {draft},
year = 2006
}
@incollection{monin06:_iste,
author = {Jean-Fran\c{c}ois Monin and Philippe Chavin},
title = {{Coq}},
booktitle = {{Software Specification Methods, An Overview Using a Case Study}},
publisher = {Herm\`es Science},
url = {https://www.iste.co.uk/index.php?f=a&ACTION=View&id=100},
year = 2006,
editor = {H. Habrias and M. Frappier},
series = {ISTE},
chapter = 16,
isbn = {1905209347},
month = apr
}
@incollection{monincourant07:_tfp,
author = {Jean-Fran\c{c}ois Monin and Judica\"el Courant},
title = {{Proving Termination Using Dependent Types: the Case of Xor-Terms}},
editor = {H. Nilsson},
booktitle = {{Trends in Functional Programming 7}},
pages = {1-18},
chapter = 1,
publisher = {Intellect},
address = {Bristol, UK / Chicago, USA},
year = 2007,
month = apr
}
@inproceedings{courantmonin06wits,
author = {Judica{\"e}l Courant and Jean-Fran\c{c}ois Monin},
title = {Defending the bank with a proof assistant},
booktitle = {{WITS 2006}},
note = {In {WITS} proceedings},
year = 2006,
address = {Vienna},
month = mar
}
@book{livre-mf-trad,
author = {J-F. Monin},
title = {Understanding Formal Methods},
publisher = {Springer Verlag},
note = {Foreword by G. Huet, ISBN 1-85233-247-6},
year = 2002
}
@inproceedings{join_calcul_TT,
author = {Jean-Fran\c{c}ois Monin},
title = {{Formalisation of the Join-Calculus in Type Theory}},
booktitle = {{International Worshop on Formal Methods and Security}},
year = 2004,
month = may,
editor = {P-L. Curien and Song Fangmin},
address = {Nankin}
}
@inproceedings{tphols04,
author = {Jean-Fran\c{c}ois Monin},
title = {{Proof pearl: From concrete to functional unparsing}},
booktitle = {{Theorem Proving in Higher Order Logics
(17th International Conference on TPHOLs 2004)}},
pages = {217--224},
publisher = {Springer Verlag},
month = {September},
address = {Park City, Utah, USA},
year = 2004,
editor = {K. Slind and A. Bunker and G. Gopalakrishnan},
volume = 3223,
series = {LNCS}
}
@inproceedings{courantmonin06jfla,
author = {Judica{\"e}l Courant and Jean-Fran\c{c}ois Monin},
title = {Faire garder la banque par un {C}oq},
booktitle = {Actes des dix-septi{\`{e}}mes journ{\'{e}}es francophones des langages applicatifs},
year = 2006,
month = jan,
pages = {25 -- 39}
}
@article{fmsd-abr03,
author = {B.~B\'erard and L. Fribourg and F.~Klay and J-F.~Monin},
title = {A compared study of two correctness proofs for
the standardized algorithm of {ABR} conformance},
journal = {{Formal Methods in System Design}},
year = 2003,
volume = 22,
month = jan,
pages = {59--86}
}
@article{fmsd-abr00,
author = {J-F.~Monin},
title = {Proving the Correctness of
the Standardized Algorithm for {ABR} conformance},
journal = {{Formal Methods in System Design}},
year = 2000,
volume = 17,
month = dec,
pages = {221--243}
}
@incollection{Monin-Klay-abr-99,
author = {J-F. Monin and F. Klay},
title = {{Correctness Proof of the Standardized Algorithm for
ABR Conformance}},
booktitle = {{FM'99 -- Formal Methods}},
publisher = {Springer Verlag},
year = 1999,
editor = {Jeannette Wing and Jim Woodcock and Jim Davies},
volume = 1708,
pages = {662--681},
series = {LNCS}
}
@incollection{jfm-abr-98,
author = {J-F. Monin},
title = {{Proving a real time algorithm for ATM in Coq}},
booktitle = {{Types for Proofs and Programs}},
publisher = {Springer Verlag},
year = 1998,
editor = {E. Gimenez and C. Paulin-Mohring},
volume = 1512,
pages = {277--293},
series = {LNCS}
}
@incollection{facit-invoice,
author = {P. Chavin and J-F. Monin},
editor = {Marc Frappier and Henri Habrias},
booktitle = {Software Specification Methods},
title = {{An Abstract and constructive specification in Coq}},
chapter = 13,
publisher = {Springer Verlag},
year = 2000,
series = {FACIT}
}
@article{jfm-scp-96,
author = {J-F. Monin},
title = {{Exceptions considered harmless}},
journal = {{Science of Computer Programming}},
year = 1996,
volume = 26,
pages = {179--196}
}
@incollection{jfm-mpc-95,
author = {J-F. Monin},
title = {{Extracting Programs with Exceptions
in an Impredicative Type System}},
booktitle = {{Mathematics of Program Construction}},
publisher = {Springer Verlag},
year = 1995,
editor = {B. M{\"o}ller},
volume = 947,
series = {LNCS}
}
@article{JMG-ieee-88,
author = {C. Jard and J-F. Monin and R. Groz},
title = {Development of {V}eda, a {P}rototyping {T}ool for
{D}istributed {A}lgorithms},
journal = {IEEE Transactions on Software Engineering},
volume = 14,
number = 3,
pages = {339--352},
month = mar,
year = 1988,
keywords = {Parallel Programming}
}
@inproceedings{JaGrMo-86,
author = {C. Jard and R. Groz and J-F. Monin},
title = {V\'eda: a {}Software {S}imulator for the {V}alidation of
{P}rotocol {S}pecifications},
editor = {L. Csaba and K. Tarnay and T. Szentivanyi},
booktitle = {COMNET'85, Computer Network Usage: Recent Experiences},
year = 1986,
publisher = {North Holland},
address = {Budapest}
}
@inproceedings{JaMoGr-86,
author = {C. Jard and J-F. Monin and R. Groz },
title = {Experience in implementing {X250} (a {CCITT} Subset of
{Estelle})},
booktitle = {IFIP Workshop V on Protocol Specification Testing
and Verification},
publisher = {North Holland},
year = 1986,
editor = {M. Diaz}
}
@inproceedings{jfm-plilp-88,
author = {J-F. Monin},
title = {A Compiler Written in {P}rolog: the {V}\'eda Experience},
booktitle = {Programming Languages Implementation and Logic Programming},
publisher = {Springer Verlag},
year = 1989,
editor = {Deransart and Lorho and Maluszynski},
number = 348,
series = {LNCS},
address = {Orl\'eans}
}
@inproceedings{glmphrcl-89,
author = {R. Groz and M. Litime and J-F. Monin and M. Phalippou
and C. Herv\'e and P. Riou and P. Cousin and J. Le
Compagnon},
title = {Elements of a {C.A.S.E.} Environment for Defining and
Generating Test Suites},
booktitle = {Int. Work. on Prot. Test Syst},
year = 1989,
address = {Berlin}
}
@inproceedings{jfm-iclp-91,
author = {J-F. Monin},
title = {Real-size Compiler Writing Using {P}rolog with
Arrows},
pages = {188--201},
booktitle = {Proceedings of the Eighth International Conference on
Logic Programming},
year = 1991,
editor = {Koichi Furukawa},
publisher = {The MIT Press},
address = {Paris, France}
}
@inproceedings{GdJfm-fme-93,
author = {G. Doumenc and J-F. Monin},
title = {The Parallel Abstract Machine : A Common Execution
Model for {FDT}s},
booktitle = {FME'93 : Industrial-Strength Formal Methods},
publisher = {Springer Verlag},
year = 1993,
volume = 670,
series = {LNCS}
}
@inproceedings{jfm-prol-84,
author = {J-F. Monin},
title = {\'Ecriture d'un compilateur r\'eel en {P}rolog},
booktitle = {S\'eminaire sur la programmation en logique},
year = 1984,
editor = {S. Bourgault and M. Dincbas},
address = {Plestin}
}
@inproceedings{aya-estelle,
author = {J-M. Ayache and R. Groz and C. Jard and J-F. Monin},
title = {Des outils pour {Estelle} : du prototype au poste industriel},
booktitle = {Journ\'ees francophones pour l'informatique},
year = 1987,
month = jan,
note = {Li\`ege}
}
@inproceedings{ZhMo-cfip-88,
author = {W. Zhang and J-F. Monin},
title = {R\'esultats et exp\'eriences sur un environnement de
simulation pour l'\'evaluation de performances \`a
partir d'{Estelle}},
booktitle = {Colloque Francophone sur l'Ing\'enierie des Protocoles},
year = 1988,
editor = {R. Castanet and O. Rafiq},
address = {Bordeaux}
}
@incollection{jfm-c3-85,
author = {J-F. Monin},
title = {Terminaison distribu\'ee et groupes commutatifs},
booktitle = {Parall\'elisme, communication et synchronisation},
publisher = {\'editions du CNRS},
year = 1985,
editor = {J-P. Verjus and G. Roucairol}
}
@book{condillac,
author = {M. Condillac},
title = {Prolog, fondements et applications},
publisher = {Dunod},
year = 1986,
note = {r\'edacteur de deux chapitres}
}
@book{livref,
editor = {F. du Castel},
title = {{L}es {t\'el\'ecommunications}},
publisher = {Roger Levrault Int.},
year = 1993,
note = {contribution au chapitre informatique}
}
@article{BCM-95,
author = {P. Bellot and J.-P. Cottin and
J-F. Monin},
title = {{D\'eveloppement et validation de logiciels.
M\'ethodes formelles}},
journal = {{Techniques de l'Ing\'enieur}},
year = 1995,
number = 12,
pages = {1--12}
}
@inbook{ofta-97,
author = {J-F. Monin and J. Sifakis},
title = {Application des techniques formelles au logiciel},
chapter = {II, El\'ements de classification des m\'ethodes formelles},
publisher = {OFTA},
year = 1997,
volume = 20,
series = {Arago}
}
@phdthesis{jfm-these,
author = {J-F. Monin},
title = {Programmation en logique et compilation de
protocoles : le simulateur V\'eda},
school = {Universit\'e de Rennes I},
type = {Th\`ese d'universit\'e},
year = 1989,
month = jan
}
@phdthesis{jfm-hdr,
author = {J-F. Monin},
title = {Contribution aux m\'ethodes formelles pour le logiciel},
school = {Universit\'e de Paris Sud},
type = {M\'emoire d'habilitation \`a diriger des recherches},
year = 2002,
month = apr
}
This file was generated by bibtex2html 1.98.