The SCEAS System
| |||||||

## Search the dblp DataBase
Benjamin Grégoire:
[Publications]
[Author Rank by year]
[Co-authors]
[Prefers]
[Cites]
[Cited by]
## Publications of Author- 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] - 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] - 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] - Benjamin Grégoire, Xavier Leroy
**A compiled implementation of strong reduction.**[Citation Graph (0, 0)][DBLP] ICFP, 2002, pp:235-246 [Conf] - 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] - 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] - 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] - 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] - 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] **Preservation of Proof Obligations from Java to the Java Virtual Machine.**[Citation Graph (, )][DBLP]**A Machine-Checked Formalization of Sigma-Protocols.**[Citation Graph (, )][DBLP]**Type-Based Termination with Sized Products.**[Citation Graph (, )][DBLP]**The MOBIUS Proof Carrying Code Infrastructure.**[Citation Graph (, )][DBLP]**JACK - A Tool for Validation of Security and Behaviour of Java Applications.**[Citation Graph (, )][DBLP]**Implementing a Direct Method for Certificate Translation.**[Citation Graph (, )][DBLP]**Formal Certification of ElGamal Encryption.**[Citation Graph (, )][DBLP]**Formal certification of code-based cryptographic proofs.**[Citation Graph (, )][DBLP]**Formally Certifying the Security of Digital Signature Schemes.**[Citation Graph (, )][DBLP]**Combining a Verification Condition Generator for a Bytecode Language with Static Analyses.**[Citation Graph (, )][DBLP]**MOBIUS: Mobility, Ubiquity, Security.**[Citation Graph (, )][DBLP]**A New Elimination Rule for the Calculus of Inductive Constructions.**[Citation Graph (, )][DBLP]**A Tutorial on Type-Based Termination.**[Citation Graph (, )][DBLP]**Programming Language Techniques for Cryptographic Proofs.**[Citation Graph (, )][DBLP]**Extending Coq with Imperative Features and Its Application to SAT Verification.**[Citation Graph (, )][DBLP]
Search in 0.003secs, Finished in 0.004secs | |||||||

| |||||||

| |||||||

System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002 for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002 |