The SCEAS System
Navigation Menu

Search the dblp DataBase

Title:
Author:

Benjamin Grégoire: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

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]


Search in 0.003secs, Finished in 0.004secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002