simpl_index.bib

@comment{{This file has been generated by bib2bib 1.98}}
@comment{{Command line: /usr/bin/bib2bib -oc simpl_index.bib.liste -ob simpl_index.bib --remove abstract --remove pdf --remove ps index.bib}}
@incollection{mifi17,
  author = {Vania Joloboff and
               Jean-Fran\c{c}ois Monin and
               Xiaomu Shi},
  title = {{SimSoC: A Fast, Proven Faithful, Full System Virtual Prototyping Framework}},
  booktitle = {{Model-Implementation Fidelity in Cyber Physical System Design}},
  year = 2017,
  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 = {http://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},
  urlpdf = {http://hal.inria.fr/inria-00489412/PDF/paper_1.pdf}
}
@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 = {http://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 = {http://arxiv.org/abs/0907.3599},
  bibsource = {DBLP, http://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 = {http://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.