Search the dblp DataBase

Publications of Author

1. Benjamin Grégoire, Laurent Théry
   A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. [Citation Graph (0, 0)][DBLP]
   IJCAR, 2006, pp:423-437 [Conf]
   
2. Bruno Barras, Benjamin Grégoire
   On the Role of Type Decorations in the Calculus of Inductive Constructions. [Citation Graph (0, 0)][DBLP]
   CSL, 2005, pp:151-166 [Conf]
   
3. Benjamin Grégoire, Laurent Théry, Benjamin Werner
   A Computational Approach to Pocklington Certificates in Type Theory. [Citation Graph (0, 0)][DBLP]
   FLOPS, 2006, pp:97-113 [Conf]
   
4. Benjamin Grégoire, Xavier Leroy
   A compiled implementation of strong reduction. [Citation Graph (0, 0)][DBLP]
   ICFP, 2002, pp:235-246 [Conf]
   
5. Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
   CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. [Citation Graph (0, 0)][DBLP]
   LPAR, 2006, pp:257-271 [Conf]
   
6. Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk
   Certificate Translation for Optimizing Compilers. [Citation Graph (0, 0)][DBLP]
   SAS, 2006, pp:301-317 [Conf]
   
7. Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
   Practical Inference for Type-Based Termination in a Polymorphic Setting. [Citation Graph (0, 0)][DBLP]
   TLCA, 2005, pp:71-85 [Conf]
   
8. Benjamin Grégoire, Assia Mahboubi
   Proving Equalities in a Commutative Ring Done Right in Coq. [Citation Graph (0, 0)][DBLP]
   TPHOLs, 2005, pp:98-113 [Conf]
   
9. Yves Bertot, Benjamin Grégoire, Xavier Leroy
   A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. [Citation Graph (0, 0)][DBLP]
   TYPES, 2004, pp:66-81 [Conf]
   
10. 
    Preservation of Proof Obligations from Java to the Java Virtual Machine. [Citation Graph (, )][DBLP]
    
    
11. 
    A Machine-Checked Formalization of Sigma-Protocols. [Citation Graph (, )][DBLP]
    
    
12. 
    Type-Based Termination with Sized Products. [Citation Graph (, )][DBLP]
    
    
13. 
    The MOBIUS Proof Carrying Code Infrastructure. [Citation Graph (, )][DBLP]
    
    
14. 
    JACK - A Tool for Validation of Security and Behaviour of Java Applications. [Citation Graph (, )][DBLP]
    
    
15. 
    Implementing a Direct Method for Certificate Translation. [Citation Graph (, )][DBLP]
    
    
16. 
    Formal Certification of ElGamal Encryption. [Citation Graph (, )][DBLP]
    
    
17. 
    Formal certification of code-based cryptographic proofs. [Citation Graph (, )][DBLP]
    
    
18. 
    Formally Certifying the Security of Digital Signature Schemes. [Citation Graph (, )][DBLP]
    
    
19. 
    Combining a Verification Condition Generator for a Bytecode Language with Static Analyses. [Citation Graph (, )][DBLP]
    
    
20. 
    MOBIUS: Mobility, Ubiquity, Security. [Citation Graph (, )][DBLP]
    
    
21. 
    A New Elimination Rule for the Calculus of Inductive Constructions. [Citation Graph (, )][DBLP]
    
    
22. 
    A Tutorial on Type-Based Termination. [Citation Graph (, )][DBLP]
    
    
23. 
    Programming Language Techniques for Cryptographic Proofs. [Citation Graph (, )][DBLP]
    
    
24. 
    Extending Coq with Imperative Features and Its Application to SAT Verification. [Citation Graph (, )][DBLP]