@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.