| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin |
Verified Indifferentiable Hashing into Elliptic Curves.  |
POST  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin |
Probabilistic relational reasoning for differential privacy. |
POPL |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Livshits, Riccardo Scandariato (eds.) |
Engineering Secure Software and Systems - 4th International Symposium, ESSoS 2012, Eindhoven, The Netherlands, February, 16-17, 2012. Proceedings |
ESSoS |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Delphine Demange, David Pichardie |
A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. |
ESOP |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk |
Secure information flow by self-composition. |
Mathematical Structures in Computer Science |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Boris Köpf |
Information-theoretic Bounds for Differentially Private Mechanisms. |
IACR Cryptology ePrint Archive |
2011 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, César Kunz |
An Abstract Model of Certificate Translation. |
ACM Trans. Program. Lang. Syst. |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Alberto Pardo, Gerardo Schneider (eds.) |
Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings |
SEFM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jorge Cuéllar, Javier Lopez, Gilles Barthe, Alexander Pretschner (eds.) |
Security and Trust Management - 6th International Workshop, STM 2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers |
STM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Federico Olmedo, Santiago Zanella Béguelin |
Verifiable Security of Boneh-Franklin Identity-Based Encryption. |
ProvSec |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella Béguelin |
Beyond Provable Security Verifiable IND-CCA Security of OAEP. |
CT-RSA |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Boris Köpf |
Information-Theoretic Bounds for Differentially Private Mechanisms. |
CSF |
2011 |
DBLP DOI BibTeX RDF |
Quantitative Information-Flow, Information Theory, Differential Privacy |
| 1 | Gilles Barthe, Juan Manuel Crespo, César Kunz |
Relational Verification Using Product Programs. |
FM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna |
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. |
FM |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin |
Computer-Aided Security Proofs for the Working Cryptographer. |
CRYPTO |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Mathilde Duclos, Yassine Lakhnech |
A Computational Indistinguishability Logic for the Bounded Storage Model. |
FPS |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe (eds.) |
Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings |
ESOP |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld |
Security of multithreaded programs by compilation. |
ACM Trans. Inf. Syst. Secur. |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte |
On the Equality of Probabilistic Terms. |
LPAR (Dakar) |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin |
Programming Language Techniques for Cryptographic Proofs. |
ITP |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk, Bogdan Warinschi |
Robustness Guarantees for Anonymity. |
CSF |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Grégoire, Sylvain Heraud |
A Machine-Checked Formalization of Sigma-Protocols. |
CSF |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Pablo Buiras, César Kunz |
A Functional Framework for Result Checking. |
FLOPS |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, César Kunz |
Perspectives in Certificate Translation. |
TGC |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Manuel V. Hermenegildo (eds.) |
Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings |
VMCAI |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech |
Computational indistinguishability logic. |
ACM Conference on Computer and Communications Security |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk |
Certificate translation for optimizing compilers. |
ACM Trans. Program. Lang. Syst. |
2009 |
DBLP DOI BibTeX RDF |
static analysis, program verification, program optimizations, Proof-carrying code |
| 1 | Santiago Zanella Béguelin, Gilles Barthe, Benjamin Grégoire, Federico Olmedo |
Formally Certifying the Security of Digital Signature Schemes. |
IEEE Symposium on Security and Privacy |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet |
Implementing a Direct Method for Certificate Translation. |
ICFEM |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin |
Formal certification of code-based cryptographic proofs. |
POPL |
2009 |
DBLP DOI BibTeX RDF |
cryptographic proofs, relational hoare logic, program transformations, observational equivalence, coq proof assistant |
| 1 | Alessandro Aldini, Gilles Barthe, Roberto Gorrieri (eds.) |
Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures |
FOSAD |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Frank S. de Boer (eds.) |
Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings |
FMOODS |
2008 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Colin Riba |
A Tutorial on Type-Based Termination. |
LerNet ALFA Summer School |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese |
Preservation of Proof Pbligations for Hybrid Verification Methods. |
SEFM |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe |
Certificate Translation. |
VERIFY |
2008 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Mariela Pavlova |
Preservation of Proof Obligations from Java to the Java Virtual Machine. |
IJCAR |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin |
Formal Certification of ElGamal Encryption. |
Formal Aspects in Security and Trust |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, César Kunz |
An Introduction to Certificate Translation. |
FOSAD |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, César Kunz |
Certificate translation for specification-preserving advices. |
FOAL |
2008 |
DBLP DOI BibTeX RDF |
AOP, program verification, proof-carrying code |
| 1 | Gilles Barthe, Salvador Cavadini, Tamara Rezk |
Tractable Enforcement of Declassification Policies. |
CSF |
2008 |
DBLP DOI BibTeX RDF |
type systems, declassification, information flow security |
| 1 | Gilles Barthe, César Kunz, Jorge Luis Sacchini |
Certified Reasoning in Memory Hierarchies. |
APLAS |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Cédric Fournet (eds.) |
Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers |
TGC |
2008 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Colin Riba |
Type-Based Termination with Sized Products. |
CSL |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, César Kunz |
Certificate Translation in Abstract Interpretation. |
ESOP |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Leonor Prensa Nieto |
Secure information flow for a concurrent language with scheduling. |
Journal of Computer Security |
2007 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Romain Janvier, Santiago Zanella Béguelin |
Formal Certification of Code-Based Cryptographic Proofs. |
IACR Cryptology ePrint Archive |
2007 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Tamara Rezk, Amitabh Basu |
Security types preserving compilation. |
Computer Languages, Systems & Structures |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld |
07091 Executive Summary - Mobility, Ubiquity and Security. |
Mobility, Ubiquity and Security |
2007 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld (eds.) |
Mobility, Ubiquity and Security, 25.02. - 02.03.2007 |
Mobility, Ubiquity and Security |
2007 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld |
07091 Abstracts Collection - Mobility, Ubiquity and Security. |
Mobility, Ubiquity and Security |
2007 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie |
The MOBIUS Proof Carrying Code Infrastructure. |
FMCO |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, David Pichardie, Tamara Rezk |
A Certified Lightweight Non-interference Java Bytecode Verifier. |
ESOP |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld |
Security of Multithreaded Programs by Compilation. |
ESORICS |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Tamara Rezk, Martijn Warnier |
Preventing Timing Leaks Through Transactional Branching Instructions. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Thierry Coquand |
Remarks on the equational theory of non-normalizing pure type systems. |
J. Funct. Program. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Tamara Rezk, David A. Naumann |
Deriving an Information Flow Checker and Certifying Compiler for Java. |
IEEE Symposium on Security and Privacy |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Fernando Pastawski |
CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. |
LPAR |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova, Antoine Requet |
JACK - A Tool for Validation of Security and Behaviour of Java Applications. |
FMCO |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet (eds.) |
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Second International Workshop, CASSIS 2005, Nice, France, March 8-11, 2005, Revised Selected Papers |
CASSIS |
2006 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu |
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. |
FLOPS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk |
Certificate Translation for Optimizing Compilers. |
SAS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, Eric Vétillard |
MOBIUS: Mobility, Ubiquity, Security. |
TGC |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe |
A computational view of implicit coercions in type theory. |
Mathematical Structures in Computer Science |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa |
Tool-Assisted Specification and Verification of Typed Low-Level Languages. |
J. Autom. Reasoning |
2005 |
DBLP DOI BibTeX RDF |
virtual machine, theorem proving, Java Card, bytecode verification |
| 1 | Gilles Barthe, Benjamin Grégoire, Fernando Pastawski |
Practical Inference for Type-Based Termination in a Polymorphic Setting. |
TLCA |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Mariela Pavlova, Gerardo Schneider |
Precise Analysis of Memory Consumption using Program Logics. |
SEFM |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Tamara Rezk, Ando Saabas |
Proof Obligations Preserving Compilation. |
Formal Aspects in Security and Trust |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Guillaume Dufay |
Formal Methods for Smartcard Security. |
FOSAD |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, Traian Muntean (eds.) |
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers |
CASSIS |
2005 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Tamara Rezk |
Non-interference for a JVM-like language. |
TLDI |
2005 |
DBLP DOI BibTeX RDF |
type systems, confidentiality, low level languages |
| 1 | Gilles Barthe, Maria João Frade, E. Giménez, Luis Pinto, Tarmo Uustalu |
Type-based termination of recursive definitions. |
Mathematical Structures in Computer Science |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Peter Dybjer, Peter Thiemann |
Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming. |
J. Funct. Program. |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Jan Cederquist, Sabrina Tarento |
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. |
IJCAR |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet |
Enforcing High-Level Security Properties for Applets. |
CARDIS |
2004 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Guillaume Dufay |
A Tool-Assisted Framework for Certified Bytecode Verification. |
FASE |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Sabrina Tarento |
A Machine-Checked Formalization of the Random Oracle Model. |
TYPES |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk |
Secure Information Flow by Self-Composition. |
CSFW |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Amitabh Basu, Tamara Rezk |
Security Types Preserving Compilation: (Extended Abstract). |
VMCAI |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Leonor Prensa Nieto |
Formally verifying information flow type systems for concurrent and thread systems. |
FMSE |
2004 |
DBLP DOI BibTeX RDF |
machine-checked proofs, concurrency, noninterference |
| 1 | Gilles Barthe, Venanzio Capretta, Olivier Pons |
Setoids in type theory. |
J. Funct. Program. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori |
Pure patterns type systems. |
POPL |
2003 |
DBLP DOI BibTeX RDF |
Curry-Howard, pure type systems, patterns, matching, logics, Lambda-calculus, rewriting |
| 1 | Gilles Barthe, Sorin Stratulat |
Validation of the JavaCard Platform with Implicit Induction Techniques. |
RTA |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Peter Thiemann |
Preface. |
Electr. Notes Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa |
Tool-Assisted Specification and Verification of the JavaCard Platform. |
AMAST |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Tarmo Uustalu |
CPS translating inductive and coinductive types. |
PEPM |
2002 |
DBLP DOI BibTeX RDF |
classical logic and control, inductive and coinductive types, typed ?-calculi, dependent types, CPS translations |
| 1 | Gilles Barthe, Dilian Gurov, Marieke Huisman |
Compositional Verification of Secure Applet Interactions. |
FASE |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Pierre Courtieu |
Efficient Reasoning about Executable Specifications in Coq. |
TPHOLs |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa |
A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. |
VMCAI |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Peter Dybjer, Luis Pinto, João Saraiva (eds.) |
Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures |
APPSEM |
2002 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, John Hatcliff, Morten Heine Sørensen |
Weak normalization implies strong normalization in a class of non-dependent pure type systems. |
Theor. Comput. Sci. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, John Hatcliff, Morten Heine Sørensen |
An induction principle for pure type systems. |
Theor. Comput. Sci. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Guillaume Dufay, Marieke Huisman, Simão Melo de Sousa |
Jakarta: A Toolset for Reasoning about JavaCard. |
E-smart |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Olivier Pons |
Type Isomorphisms and Proof Reuse in Dependent Type Theory. |
FoSSaCS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard P. Serpette, Simão Melo de Sousa |
A Formal Executable Semantics of the JavaCard Platform. |
ESOP |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Morten Heine Sørensen |
Domain-free pure type systems. |
J. Funct. Program. |
2000 |
DBLP BibTeX RDF |
|
| 1 | Gilles Barthe, Bernard P. Serpette |
Static Reduction Analysis for Imperative Object Oriented Languages. |
LPAR |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Femke van Raamsdonk |
Constructor Subtyping in the Calculus of Inductive Constructions. |
FoSSaCS |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Thierry Coquand |
An Introduction to Dependent Type Theory. |
APPSEM |
2000 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe |
Order-Sorted Inductive Types. |
Inf. Comput. |
1999 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, John Hatcliff, Morten Heine Sørensen |
CPS Translations and Applications: The Cube and Beyond. |
Higher-Order and Symbolic Computation |
1999 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")