Benjamin Grégoire

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeer - CSB - Google - MSN - Yahoo

18EEGilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin: Formal certification of code-based cryptographic proofs. POPL 2009: 90-101
17EEGilles Barthe, Benjamin Grégoire, Colin Riba: Type-Based Termination with Sized Products. CSL 2008: 493-507
16EEGilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin: Formal Certification of ElGamal Encryption. Formal Aspects in Security and Trust 2008: 1-19
15EEGilles Barthe, Benjamin Grégoire, Mariela Pavlova: Preservation of Proof Obligations from Java to the Java Virtual Machine. IJCAR 2008: 83-99
14EEGilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie: The MOBIUS Proof Carrying Code Infrastructure. FMCO 2007: 1-24
13EEBenjamin Grégoire, Jorge Luis Sacchini: Combining a Verification Condition Generator for a Bytecode Language with Static Analyses. TGC 2007: 23-40
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
11EEBenjamin Grégoire, Laurent Théry, Benjamin Werner: A Computational Approach to Pocklington Certificates in Type Theory. FLOPS 2006: 97-113
10EEGilles 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
9EEBenjamin Grégoire, Laurent Théry: A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. IJCAR 2006: 423-437
8EEGilles Barthe, Benjamin Grégoire, Fernando Pastawski: CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. LPAR 2006: 257-271
7EEGilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk: Certificate Translation for Optimizing Compilers. SAS 2006: 301-317
6EEGilles 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
5EEBruno Barras, Benjamin Grégoire: On the Role of Type Decorations in the Calculus of Inductive Constructions. CSL 2005: 151-166
4EEGilles Barthe, Benjamin Grégoire, Fernando Pastawski: Practical Inference for Type-Based Termination in a Polymorphic Setting. TLCA 2005: 71-85
3EEBenjamin Grégoire, Assia Mahboubi: Proving Equalities in a Commutative Ring Done Right in Coq. TPHOLs 2005: 98-113
2EEYves Bertot, Benjamin Grégoire, Xavier Leroy: A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES 2004: 66-81
1EEBenjamin Grégoire, Xavier Leroy: A compiled implementation of strong reduction. ICFP 2002: 235-246

Coauthor Index

1Bruno Barras [5]
2Gilles Barthe [4] [6] [7] [8] [10] [12] [14] [15] [16] [17] [18]
3Santiago Zanella Béguelin [16] [18]
4Lennart Beringer [6]
5Yves Bertot [2]
6Lilian Burdy [10]
7Julien Charles [10]
8Pierre Crégut [6] [14]
9Sylvain Heraud [16]
10Martin Hofmann [6]
11Marieke Huisman [10] [12]
12Thomas P. Jensen [14]
13César Kunz [7]
14Jean-Louis Lanet [10] [12]
15Xavier Leroy [1] [2]
16Assia Mahboubi [3]
17Peter Müller [6]
18Fernando Pastawski [4] [8]
19Mariela Pavlova [10] [15]
20David Pichardie [14]
21Erik Poll [6]
22Germán Puebla (German Puebla) [6]
23Antoine Requet [10]
24Tamara Rezk [7]
25Colin Riba [17]
26Jorge Luis Sacchini [13]
27Ian Stark [6]
28Laurent Théry [9] [11]
29Eric Vétillard [6]
30Benjamin Werner [11]

Colors in the list of coauthors

Copyright © Sun May 17 03:24:02 2009 by Michael Ley (ley@uni-trier.de)