KIND_INPROCEEDING.bib

@comment{{This file has been generated by bib2bib 1.97}}
@comment{{Command line: bib2bib --expand-xrefs -oc Publi/KIND_INPROCEEDING.cite -ob Publi/KIND_INPROCEEDING.bib -c '$type = "INPROCEEDINGS"' -c !topic="NOCITE" Publi/bibdata.bib}}
@inproceedings{DBLP:conf/popl/BartheFGSSB14,
  isbn = {978-1-4503-2544-8},
  publisher = {ACM},
  editor = {Suresh Jagannathan and
               Peter Sewell},
  author = {Gilles Barthe and
               C{\'e}dric Fournet and
               Benjamin Gr{\'e}goire and
               Pierre-Yves Strub and
               Nikhil Swamy and
               Santiago Zanella B{\'e}guelin},
  title = {Probabilistic relational verification for cryptographic
               implementations},
  booktitle = {POPL},
  year = {2014},
  pages = {193-206},
  ee = {http://doi.acm.org/10.1145/2535838.2535847},
  topic = {CRYPTO},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/ccs/BartheCGKLSB13,
  isbn = {978-1-4503-2477-9},
  publisher = {ACM},
  editor = {Ahmad-Reza Sadeghi and
               Virgil D. Gligor and
               Moti Yung},
  author = {Gilles Barthe and
               Juan Manuel Crespo and
               Benjamin Gr{\'e}goire and
               C{\'e}sar Kunz and
               Yassine Lakhnech and
               Benedikt Schmidt and
               Santiago Zanella B{\'e}guelin},
  title = {Fully automated analysis of padding-based encryption in
               the computational model},
  booktitle = {ACM Conference on Computer and Communications Security},
  year = {2013},
  pages = {1247-1260},
  ee = {http://doi.acm.org/10.1145/2508859.2516663},
  topic = {CRYPTO},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/csfw/BartheDGKB13,
  isbn = {978-0-7695-5031-2},
  publisher = {IEEE},
  author = {Gilles Barthe and
               George Danezis and
               Benjamin Gr{\'e}goire and
               C{\'e}sar Kunz and
               Santiago Zanella B{\'e}guelin},
  title = {Verified Computational Differential Privacy with Applications
               to Smart Metering},
  booktitle = {CSF},
  year = {2013},
  pages = {287-301},
  ee = {http://dx.doi.org/10.1109/CSF.2013.26},
  topic = {CRYPTO},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/cpp/BartheGKLB12,
  isbn = {978-3-642-35307-9},
  volume = {7679},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Chris Hawblitzel and
               Dale Miller},
  author = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               C{\'e}sar Kunz and
               Yassine Lakhnech and
               Santiago Zanella B{\'e}guelin},
  title = {Automation in Computer-Aided Cryptography: Proofs, Attacks
               and Designs},
  booktitle = {CPP},
  year = {2012},
  pages = {7-8},
  ee = {http://dx.doi.org/10.1007/978-3-642-35308-6_3},
  topic = {CRYPTO},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/csfw/BackesBBGKSB12,
  isbn = {978-1-4673-1918-8},
  publisher = {IEEE},
  editor = {Stephen Chong},
  author = {Michael Backes and
               Gilles Barthe and
               Matthias Berg and
               Benjamin Gr{\'e}goire and
               C{\'e}sar Kunz and
               Malte Skoruppa and
               Santiago Zanella B{\'e}guelin},
  title = {Verified Security of Merkle-Damg{\aa}rd},
  booktitle = {CSF},
  year = {2012},
  pages = {354-368},
  ee = {http://doi.ieeecomputersociety.org/10.1109/CSF.2012.14},
  topic = {CRYPTO},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/itp/BartheCGKB12,
  isbn = {978-3-642-32346-1},
  volume = {7406},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Lennart Beringer and
               Amy P. Felty},
  author = {Gilles Barthe and
               Juan Manuel Crespo and
               Benjamin Gr{\'e}goire and
               C{\'e}sar Kunz and
               Santiago Zanella B{\'e}guelin},
  title = {Computer-Aided Cryptographic Proofs},
  booktitle = {ITP},
  year = {2012},
  pages = {11-27},
  ee = {http://dx.doi.org/10.1007/978-3-642-32347-8_2},
  topic = {CRYPTO},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/post/BartheGHOB12,
  isbn = {978-3-642-28640-7},
  volume = {7215},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Pierpaolo Degano and
               Joshua D. Guttman},
  author = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               Sylvain Heraud and
               Federico Olmedo and
               Santiago Zanella B{\'e}guelin},
  title = {Verified Indifferentiable Hashing into Elliptic Curves},
  booktitle = {POST},
  year = {2012},
  pages = {209-228},
  ee = {http://dx.doi.org/10.1007/978-3-642-28641-4_12},
  topic = {CRYPTO},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/sas/BartheGB12,
  isbn = {978-3-642-33124-4},
  volume = {7460},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Antoine Min{\'e} and
               David Schmidt},
  author = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               Santiago Zanella B{\'e}guelin},
  title = {Computer-Aided Cryptographic Proofs},
  booktitle = {SAS},
  year = {2012},
  pages = {1-2},
  ee = {http://dx.doi.org/10.1007/978-3-642-33125-1_1},
  topic = {CRYPTO},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@inproceedings{DBLP:conf/adg/GregoirePT08,
  author = {Benjamin Gr{\'e}goire and
               Lo\"{\i}c Pottier and
               Laurent Th{\'e}ry},
  title = {Proof Certificates for Algebra and Their Application to
               Automatic Geometry Theorem Proving},
  booktitle = {Automated Deduction in Geometry - 7th International Workshop,
               ADG 2008, Shanghai, China, September 22-24, 2008. Revised
               Papers},
  pages = {42-59},
  ee = {http://dx.doi.org/10.1007/978-3-642-21046-4_3},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6301},
  year = {2011},
  isbn = {978-3-642-21045-7},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  topic = {COQAPPLI}
}
@inproceedings{BDG11,
  author = {Mathieu Boespflug and Maxime D{\'e}n{\`e}s and Benjamin Gr{\'e}goire},
  title = {Full reduction at full throttle},
  booktitle = {First International Conference on Certified Programs and Proofs, 
               Tawain, December 7-9},
  year = {2011},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  topic = {COMPILER}
}
@inproceedings{AFGKTW11,
  author = {Michael Armand and Germain Faure and Benjamin Gr{\'e}goire and Chantal Keller and
               Laurent Th{\'e}ry and Benjamin Werner},
  title = {A Modular Integration of SAT/SMT Solvers to 
               Coq through Proof Witnesses},
  booktitle = {First International Conference on Certified Programs and Proofs, 
               Tawain, December 7-9},
  year = {2011},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  topic = {COMPILER},
  note = {To Appear}
}
@inproceedings{DBLP:conf/crypto/BartheGHB11,
  author = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               Sylvain Heraud and
               Santiago Zanella B{\'e}guelin},
  title = {Computer-Aided Security Proofs for the Working Cryptographer},
  booktitle = {Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology
               Conference, Santa Barbara, CA, USA, August 14-18, 2011.
               Proceedings},
  year = {2011},
  pages = {71-90},
  ee = {http://dx.doi.org/10.1007/978-3-642-22792-9_5},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6841},
  isbn = {978-3-642-22791-2},
  topic = {CRYPTO},
  note = {Best Paper Award}
}
@inproceedings{DBLP:conf/ctrsa/BartheGLB11,
  author = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               Yassine Lakhnech and
               Santiago Zanella B{\'e}guelin},
  title = {Beyond Provable Security Verifiable IND-CCA Security of
               OAEP},
  booktitle = {Topics in Cryptology - CT-RSA 2011 - The Cryptographers'
               Track at the RSA Conference 2011, San Francisco, CA, USA,
               February 14-18, 2011. Proceedings},
  volume = {6558},
  year = {2011},
  isbn = {978-3-642-19073-5},
  pages = {180-196},
  ee = {http://dx.doi.org/10.1007/978-3-642-19074-2_13},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  publisher = {Springer},
  topic = {CRYPTO}
}
@inproceedings{DBLP:conf/lpar/GregoireS10,
  author = {Benjamin Gr{\'e}goire and
               Jorge Luis Sacchini},
  title = {On Strong Normalization of the Calculus of Constructions
               with Type-Based Termination},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning
               - 17th International Conference, LPAR-17, Yogyakarta, Indonesia,
               October 10-15, 2010. Proceedings},
  year = {2010},
  pages = {333-347},
  publisher = {Springer},
  ee = {http://dx.doi.org/10.1007/978-3-642-16242-8_24},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  topic = {TYPETHEORY}
}
@inproceedings{AGT10ITP,
  author = {Micha{\"e}l Armand and Benjamin Gr{\'e}goire and Arnaud Spiwack and
               Laurent Th{\'ery}},
  title = {Extending Coq with Imperative Features
               and its Application to SAT Verication},
  booktitle = {Interactive Theorem Proving, international
               Conference, ITP 2010, Edinburgh, Scotland, July 11-14, 2010,
               Proceedings},
  year = {2010},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  topic = {COQAPPLI}
}
@inproceedings{BGZ10ITP,
  author = {Gilles Barthe and Benjamin Gr{\'e}goire and Santiago Zanella},
  title = {Programming language techniques for cryptographic proofs},
  booktitle = {Interactive Theorem Proving, international
               Conference, ITP 2010, Edinburgh, Scotland, July 11-14, 2010,
               Proceedings},
  year = {2010},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  topic = {CRYPTO}
}
@inproceedings{BGHH10CSF,
  author = {Santiago Zanella B{\'e}guelin and Gilles Barthe and Sylvain Heraud and Benjamin Gr{\'e}goire and Daniel Hedin},
  title = {A Machine-Checked Formalization of Sigma-Protocols},
  booktitle = {Computer Security Foundations Symposium, CSF 2010, Edinburgh, Scotland, July 17-19, 2010,
               Proceedings},
  year = {2010},
  publisher = {IEEE},
  topic = {CRYPTO}
}
@inproceedings{GreOlaf08,
  author = {Jan Olaf Blech and Benjamin Gr\'egoire},
  title = { Certifying Code Generation with Coq },
  booktitle = { Proceedinfs of the Workshop Compiler Optimization meets Compiler Verification (COCV 2008)},
  year = {2008},
  publisher = {ENTCS},
  topic = {COMPILER}
}
@inproceedings{GreOlaf09,
  author = {Jan Olaf Blech and Benjamin Gr\'egoire},
  title = { Using Checker Predicates in Certifying Code Generation },
  booktitle = { Proceedinfs of the Workshop Compiler Optimization meets Compiler Verification (COCV 2009)},
  year = {2009},
  publisher = {ENTCS},
  note = {To appear},
  topic = {COMPILER}
}
@inproceedings{BartheGP08,
  author = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               Mariela Pavlova},
  title = {Preservation of Proof Obligations from Java to the Java
               Virtual Machine},
  booktitle = {Automated Reasoning, 4th International Joint Conference,
               IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  year = {2008},
  pages = {83-99},
  topic = {PCC}
}
@inproceedings{BartheGR08,
  author = {Gilles Barthe and Benjamin Gr\'egoire and Colin Riba},
  title = {Type-Based Termination with Sized Products},
  booktitle = {17th EACSL Annual Conference on Computer Science Logic, 15th-19th September 2008, Bertinoro, Italy},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  year = {2008},
  topic = {TYPETHEORY}
}
@inproceedings{FMCO07,
  author = {Gilles Barthe and Pierre~Cr\'egut and Benjamin Gr\'egoire and Thomas Jensen and David Pichardie},
  title = {The MOBIUS Proof Carrying Code infrastructure},
  booktitle = {Formal Methods for Components and Objects, 6th International
               Symposium, FMCO 2007, Amsterdam, The Netherlands, 2007, Revised Lectures},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  year = {2007},
  topic = {PCC}
}
@inproceedings{GreSacchi07,
  author = {Benjamin Gr{\'e}goire and
               Jorge Luis Sacchini},
  title = {Combining a Verification Condition Generator for a Bytecode
               Language with Static Analyses},
  booktitle = {Trustworthy Global Computing, Third Symposium, TGC 2007,
               Sophia-Antipolis, France, November 5-6, 2007, Revised Selected
               Papers},
  year = {2007},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4912},
  pages = {23-40},
  topic = {PCC}
}
@inproceedings{GreTW06,
  author = {Benjamin Gr{\'e}goire and
               Laurent Th{\'e}ry and
               Benjamin Werner},
  title = {A Computational Approach to Pocklington Certificates in
               Type Theory},
  booktitle = {Functional and Logic Programming, 8th International Symposium,
               FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings},
  year = {2006},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3945},
  pages = {97-113},
  topic = {COQAPPLI}
}
@inproceedings{DBLP:conf/fmco/BartheBCGHLPR06,
  author = {Gilles Barthe and
               Lilian Burdy and
               Julien Charles and
               Benjamin Gr{\'e}goire and
               Marieke Huisman and
               Jean-Louis Lanet and
               Mariela Pavlova and
               Antoine Requet},
  title = {JACK - A Tool for Validation of Security and Behaviour of
               Java Applications},
  booktitle = {Formal Methods for Components and Objects, 5th International
               Symposium, FMCO 2006, Amsterdam, The Netherlands, November
               7-10, 2006, Revised Lectures},
  year = {2006},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4709},
  pages = {152-174},
  topic = {PCC}
}
@inproceedings{GreT06,
  author = {Benjamin Gr{\'e}goire and
               Laurent Th{\'e}ry},
  title = {A Purely Functional Library for Modular Arithmetic and Its
               Application to Certifying Large Prime Numbers},
  booktitle = {Automated Reasoning, Third International Joint Conference,
               IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4130},
  year = {2006},
  pages = {423-437},
  topic = {COQAPPLI}
}
@inproceedings{BartheGP06,
  author = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               Fernando Pastawski},
  title = {CIC\^: Type-Based Termination of Recursive Definitions
               in the Calculus of Inductive Constructions},
  booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning,
               13th International Conference, LPAR 2006, Phnom Penh, Cambodia,
               November 13-17, 2006, Proceedings},
  year = {2006},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4246},
  pages = {257-271},
  topic = {TYPETHEORY}
}
@inproceedings{BartheGKR06,
  author = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               C{\'e}sar Kunz and
               Tamara Rezk},
  title = {Certificate Translation for Optimizing Compilers},
  booktitle = {Static Analysis, 13th International Symposium, SAS 2006,
               Seoul, Korea, August 29-31, 2006, Proceedings},
  year = {2006},
  pages = {301-317},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4134},
  topic = {PCC}
}
@inproceedings{DBLP:conf/tgc/BartheBCGHMPPSV06,
  author = {Gilles Barthe and
               Lennart Beringer and
               Pierre Cr{\'e}gut and
               Benjamin Gr{\'e}goire and
               Martin Hofmann and
               Peter M{\"u}ller and
               Erik Poll and
               Germ{\'a}n Puebla and
               Ian Stark and
               Eric V{\'e}tillard},
  title = {MOBIUS: Mobility, Ubiquity, Security},
  booktitle = {Trustworthy Global Computing, Second Symposium, TGC 2006,
               Lucca, Italy, November 7-9, 2006, Revised Selected Papers},
  year = {2006},
  pages = {10-29},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4661},
  topic = {PCC}
}
@inproceedings{BartheGP05,
  author = {Gilles Barthe and
               Benjamin Gr{\'e}goire and
               Fernando Pastawski},
  title = {Practical Inference for Type-Based Termination in a Polymorphic
               Setting},
  booktitle = {Typed Lambda Calculi and Applications, 7th International
               Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings},
  year = {2005},
  pages = {71-85},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3461},
  topic = {TYPETHEORY}
}
@inproceedings{GregM05,
  author = {Benjamin Gr{\'e}goire and
               Assia Mahboubi},
  title = {Proving Equalities in a Commutative Ring Done Right in Coq},
  booktitle = {Theorem Proving in Higher Order Logics, 18th International
               Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005,
               Proceedings},
  year = {2005},
  pages = {98-113},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3603},
  topic = {COQAPPLI}
}
@inproceedings{GregL02,
  author = {Benjamin Gr{\'e}goire and
               Xavier Leroy},
  title = {A compiled implementation of strong reduction},
  booktitle = {International Conference on Functional Programming 2002},
  year = {2002},
  pages = {235-246},
  publisher = {ACM Press},
  topic = {COMPILER}
}
@inproceedings{BarrasG05,
  author = {Bruno Barras and
               Benjamin Gr{\'e}goire},
  title = {On the Role of Type Decorations in the Calculus of Inductive
               Constructions},
  booktitle = {Computer Science Logic, 19th International Workshop, CSL
               2005, 14th Annual Conference of the EACSL, Oxford, UK, August
               22-25, 2005, Proceedings},
  year = {2005},
  pages = {151-166},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3634},
  topic = {TYPETHEORY}
}
@inproceedings{BertotGL04,
  author = {Yves Bertot and
               Benjamin Gr{\'e}goire and
               Xavier Leroy},
  title = {A Structured Approach to Proving Compiler Optimizations
               Based on Dataflow Analysis},
  booktitle = {Types for Proofs and Programs, International Workshop, TYPES
               2004, Jouy-en-Josas, France, December 15-18, 2004, Revised
               Selected Papers},
  year = {2004},
  pages = {66-81},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {3839},
  topic = {COMPILER}
}
@inproceedings{BartheGHB08:FAST,
  author = {Gilles Barthe and
Benjamin Gr{\'e}goire and
Sylvain Heraud and
Santiago Zanella B{\'e}guelin},
  title = {Formal Certification of ElGamal Encryption},
  booktitle = {Formal Aspects in Security and Trust},
  year = {2008},
  pages = {1-19},
  ee = {http://dx.doi.org/10.1007/978-3-642-01465-9_1},
  topic = {CRYPTO}
}
@inproceedings{BartheGZ09,
  author = {Gilles Barthe and Benjamin Gr\'egoire and Santiago Zanella},
  title = {Formal Certification of Code-Based Cryptographic Proofs},
  booktitle = {36th symposium Principles of Programming Languages},
  publisher = {ACM Press},
  year = 2009,
  month = jan,
  url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/popl09.pdf},
  topic = {CRYPTO}
}
@inproceedings{BGOZ:2009:SP,
  author = { G. Barthe and
                  B. Gr{\'e}goire and
                  F. Olmedo and
                  S. {Zanella B{\'e}guelin}},
  title = {Formally Certifying the Security of Digital Signature Schemes},
  booktitle = {30th IEEE Symposium on Security and Privacy, S\&P 2009},
  year = {2009},
  topic = {CRYPTO}
}
@inproceedings{BGHKP:2009:ICFEM,
  author = {Gilles Barthe and
                 Benjamin Gr{\'e}goire and
                 Sylvain Heraud and
                 Cesar Kunz and
                 Anne Pacalet},
  title = {Implementing a direct method for certificate translation},
  booktitle = {International Conference on Formal Engineering Methods, ICFEM 2009},
  year = {2009},
  series = {Lectures Notes in Computer Science},
  note = {To appear},
  topic = {COMPILER}
}
@inproceedings{BarrasCGHS:Types09,
  author = {Bruno Barras and
            Pierre Corbineau and
            Benjamin Gr{\'e}goire and
            Hugo Herbelin and
            Jorge Luis Sacchini},
  title = {A New Elimination Rule for the {C}alculus of {I}nductive {C}onstructions},
  booktitle = {Types for proofs and programs 2008},
  year = {2009},
  pages = {32-48},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  editor = {S. Berardi and F. Damiani and U de'Liguoro},
  volume = {5497},
  x-proceedings = {yes},
  x-international-audience = {yes},
  x-invited-conference = {no},
  topic = {TYPETHEORY}
}

This file was generated by bibtex2html 1.97.