| * | 2009 |
| 22 | EE | 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: 237-250 |
| 21 | EE | Gilles Barthe,
Benjamin Grégoire,
Santiago Zanella Béguelin:
Formal certification of code-based cryptographic proofs.
POPL 2009: 90-101 |
| 20 | EE | Gilles Barthe,
Benjamin Grégoire,
César Kunz,
Tamara Rezk:
Certificate translation for optimizing compilers.
ACM Trans. Program. Lang. Syst. 31(5): (2009) |
| 2008 |
| 19 | EE | Gilles Barthe,
Benjamin Grégoire,
Colin Riba:
Type-Based Termination with Sized Products.
CSL 2008: 493-507 |
| 18 | EE | Gilles Barthe,
Benjamin Grégoire,
Sylvain Heraud,
Santiago Zanella Béguelin:
Formal Certification of ElGamal Encryption.
Formal Aspects in Security and Trust 2008: 1-19 |
| 17 | EE | Gilles Barthe,
Benjamin Grégoire,
Mariela Pavlova:
Preservation of Proof Obligations from Java to the Java Virtual Machine.
IJCAR 2008: 83-99 |
| 16 | EE | Gilles Barthe,
Benjamin Grégoire,
Colin Riba:
A Tutorial on Type-Based Termination.
LerNet ALFA Summer School 2008: 100-152 |
| 15 | EE | Bruno Barras,
Pierre Corbineau,
Benjamin Grégoire,
Hugo Herbelin,
Jorge Luis Sacchini:
A New Elimination Rule for the Calculus of Inductive Constructions.
TYPES 2008: 32-48 |
| 2007 |
| 14 | EE | Gilles Barthe,
Pierre Crégut,
Benjamin Grégoire,
Thomas P. Jensen,
David Pichardie:
The MOBIUS Proof Carrying Code Infrastructure.
FMCO 2007: 1-24 |
| 13 | EE | Benjamin Grégoire,
Jorge Luis Sacchini:
Combining a Verification Condition Generator for a Bytecode Language with Static Analyses.
TGC 2007: 23-40 |
| 2006 |
| 12 | | Gilles Barthe,
Benjamin Grégoire,
Marieke Huisman,
Jean-Louis Lanet:
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Second International Workshop, CASSIS 2005, Nice, France, March 8-11, 2005, Revised Selected Papers
Springer 2006 |
| 11 | EE | Benjamin Grégoire,
Laurent Théry,
Benjamin Werner:
A Computational Approach to Pocklington Certificates in Type Theory.
FLOPS 2006: 97-113 |
| 10 | EE | 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: 152-174 |
| 9 | EE | Benjamin Grégoire,
Laurent Théry:
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers.
IJCAR 2006: 423-437 |
| 8 | EE | Gilles Barthe,
Benjamin Grégoire,
Fernando Pastawski:
CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions.
LPAR 2006: 257-271 |
| 7 | EE | Gilles Barthe,
Benjamin Grégoire,
César Kunz,
Tamara Rezk:
Certificate Translation for Optimizing Compilers.
SAS 2006: 301-317 |
| 6 | EE | 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: 10-29 |
| 2005 |
| 5 | EE | Bruno Barras,
Benjamin Grégoire:
On the Role of Type Decorations in the Calculus of Inductive Constructions.
CSL 2005: 151-166 |
| 4 | EE | Gilles Barthe,
Benjamin Grégoire,
Fernando Pastawski:
Practical Inference for Type-Based Termination in a Polymorphic Setting.
TLCA 2005: 71-85 |
| 3 | EE | Benjamin Grégoire,
Assia Mahboubi:
Proving Equalities in a Commutative Ring Done Right in Coq.
TPHOLs 2005: 98-113 |
| 2004 |
| 2 | EE | Yves Bertot,
Benjamin Grégoire,
Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis.
TYPES 2004: 66-81 |
| 2002 |
| 1 | EE | Benjamin Grégoire,
Xavier Leroy:
A compiled implementation of strong reduction.
ICFP 2002: 235-246 |