Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic ScholarBenjamin Grégoire
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2020
[j6]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. J. Cryptographic Engineering 10(1): 17-26 (2020)- [j5]Gilles Barthe, Sandrine Blazy
, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu:
Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4(POPL): 7:1-7:30 (2020) - [i30]Gaëtan Cassiers, Benjamin Grégoire, Itamar Levi, François-Xavier Standaert:
Hardware Private Circuits: From Trivial Composition to Full Verification. IACR Cryptol. ePrint Arch. 2020: 185 (2020) - [i29]Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth:
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification. IACR Cryptol. ePrint Arch. 2020: 603 (2020)
2010 – 2019
- 2019
- [c66]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran:
A Machine-Checked Proof of Security for AWS Key Management Service. ACM Conference on Computer and Communications Security 2019: 63-78 - [c65]José Bacelar Almeida, Cecile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub:
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. ACM Conference on Computer and Communications Security 2019: 1607-1622 - [c64]Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub:
Symbolic Methods in Computational Cryptography Proofs. CSF 2019: 136-151 - [c63]Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert:
maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults. ESORICS (1) 2019: 300-318 - [c62]Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan:
FaCT: a DSL for timing-sensitive computation. PLDI 2019: 174-189 - [i28]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub:
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR abs/1904.04606 (2019) - [i27]Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu:
Formal Verification of a Constant-Time Preserving C Compiler. IACR Cryptol. ePrint Arch. 2019: 926 (2019) - [i26]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran:
A Machine-Checked Proof of Security for AWS Key Management Service. IACR Cryptol. ePrint Arch. 2019: 1042 (2019) - [i25]José Bacelar Almeida, Cecile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub:
Machine-Checked Proofs for Cryptographic Standards. IACR Cryptol. ePrint Arch. 2019: 1155 (2019) - 2018
- [j4]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang. 2(POPL): 57:1-57:29 (2018) - [c61]Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi:
Symbolic Proofs for Lattice-Based Cryptography. ACM Conference on Computer and Communications Security 2018: 538-555 - [c60]Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen:
Vectorizing Higher-Order Masking. COSADE 2018: 23-43 - [c59]Cecile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire:
Formal Security Proof of CMAC and Its Variants. CSF 2018: 91-104 - [c58]Gilles Barthe, Benjamin Grégoire, Vincent Laporte:
Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". CSF 2018: 328-343 - [c57]Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
An Assertion-Based Program Logic for Probabilistic Programs. ESOP 2018: 117-144 - [c56]Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi:
Masking the GLP Lattice-Based Signature Scheme at Any Order. EUROCRYPT (2) 2018: 354-384 - [i24]Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
An Assertion-Based Program Logic for Probabilistic Programs. CoRR abs/1803.05535 (2018) - [i23]Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen:
Vectorizing Higher-Order Masking. IACR Cryptol. ePrint Arch. 2018: 173 (2018) - [i22]Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi:
Masking the GLP Lattice-Based Signature Scheme at Any Order. IACR Cryptol. ePrint Arch. 2018: 381 (2018) - [i21]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations. IACR Cryptol. ePrint Arch. 2018: 505 (2018) - [i20]Gilles Barthe, Sonia Belaïd, Pierre-Alain Fouque, Benjamin Grégoire:
maskVerif: a formal tool for analyzing software and hardware masked implementations. IACR Cryptol. ePrint Arch. 2018: 562 (2018) - [i19]Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi:
Symbolic Proofs for Lattice-Based Cryptography. IACR Cryptol. ePrint Arch. 2018: 765 (2018) - 2017
- [c55]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub:
Jasmin: High-Assurance and High-Speed Cryptography. ACM Conference on Computer and Communications Security 2017: 1807-1823 - [c54]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira:
A Fast and Verified Software Stack for Secure Function Evaluation. ACM Conference on Computer and Communications Security 2017: 1989-2006 - [c53]Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. EUROCRYPT (1) 2017: 535-566 - [c52]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving uniformity and independence by self-composition and coupling. LPAR 2017: 385-403 - [c51]Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. POPL 2017: 161-174 - [i18]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving uniformity and independence by self-composition and coupling. CoRR abs/1701.06477 (2017) - [i17]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Expected Sensitivity of Probabilistic Programs. CoRR abs/1708.02537 (2017) - [i16]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira:
A Fast and Verified Software Stack for Secure Function Evaluation. IACR Cryptol. ePrint Arch. 2017: 821 (2017) - [i15]Gilles Barthe, François Dupressoir, Benjamin Grégoire:
A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'. IACR Cryptol. ePrint Arch. 2017: 1053 (2017) - [i14]Gilles Barthe, Benjamin Grégoire, Vincent Laporte:
Provably secure compilation of side-channel countermeasures. IACR Cryptol. ePrint Arch. 2017: 1233 (2017) - 2016
- [c50]Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. ACM Conference on Computer and Communications Security 2016: 55-67 - [c49]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini:
Strong Non-Interference and Type-Directed Higher-Order Masking. ACM Conference on Computer and Communications Security 2016: 116-129 - [c48]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A Program Logic for Union Bounds. ICALP 2016: 107:1-107:15 - [c47]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. LICS 2016: 749-758 - [i13]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. CoRR abs/1601.05047 (2016) - [i12]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A program logic for union bounds. CoRR abs/1602.05681 (2016) - [i11]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. CoRR abs/1606.07143 (2016) - [i10]Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. CoRR abs/1607.03455 (2016) - [i9]Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. IACR Cryptol. ePrint Arch. 2016: 912 (2016) - 2015
- [c46]Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt:
Automated Proofs of Pairing-Based Cryptography. ACM Conference on Computer and Communications Security 2015: 1156-1168 - [c45]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub:
Verified Proofs of Higher-Order Masking. EUROCRYPT (1) 2015: 457-485 - [c44]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub:
Relational Reasoning via Probabilistic Coupling. LPAR 2015: 387-401 - [i8]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub:
Relational reasoning via probabilistic coupling. CoRR abs/1509.03476 (2015) - [i7]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub:
Verified Proofs of Higher-Order Masking. IACR Cryptol. ePrint Arch. 2015: 60 (2015) - [i6]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire:
Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler. IACR Cryptol. ePrint Arch. 2015: 506 (2015) - 2014
- [c43]Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz:
Synthesis of Fault Attacks on Cryptographic Implementations. ACM Conference on Computer and Communications Security 2014: 1016-1027 - [c42]Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz:
Making RSA-PSS Provably Secure against Non-random Faults. CHES 2014: 206-222 - [c41]Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub:
Certified Synthesis of Efficient Batch Verifiers. CSF 2014: 153-165 - [c40]Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin:
Probabilistic relational verification for cryptographic implementations. POPL 2014: 193-206 - [i5]Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz:
Making RSA-PSS Provably Secure Against Non-Random Faults. IACR Cryptol. ePrint Arch. 2014: 252 (2014) - [i4]Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz:
Synthesis of Fault Attacks on Cryptographic Implementations. IACR Cryptol. ePrint Arch. 2014: 436 (2014) - [i3]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub:
Verified Implementations for Secure and Verifiable Computation. IACR Cryptol. ePrint Arch. 2014: 456 (2014) - 2013
- [j3]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin:
Verified indifferentiable hashing into elliptic curves. J. Comput. Secur. 21(6): 881-917 (2013) - [c39]Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella Béguelin:
Fully automated analysis of padding-based encryption in the computational model. ACM Conference on Computer and Communications Security 2013: 1247-1260 - [c38]Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin:
Verified Computational Differential Privacy with Applications to Smart Metering. CSF 2013: 287-301 - [c37]Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub:
EasyCrypt: A Tutorial. FOSAD 2013: 146-166 - 2012
- [c36]Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin:
Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. CPP 2012: 7-8 - [c35]Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin:
Verified Security of Merkle-Damgård. CSF 2012: 354-368 - [c34]Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin:
Computer-Aided Cryptographic Proofs. ITP 2012: 11-27 - [c33]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. MPC 2012: 1-6 - [c32]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin:
Verified Indifferentiable Hashing into Elliptic Curves. POST 2012: 209-228 - [c31]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Computer-Aided Cryptographic Proofs. SAS 2012: 1-2 - [i2]Benjamin Grégoire:
Recent Advances in the Formal Verification of Cryptographic Systems: Turing's Legacy. ERCIM News 2012(91) (2012) - [i1]Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin:
Automated Analysis and Synthesis of Padding-Based Encryption Schemes. IACR Cryptol. ePrint Arch. 2012: 695 (2012) - 2011
- [j2]Jan Olaf Blech, Benjamin Grégoire:
Certifying compilers using higher-order theorem provers as certificate checkers. Formal Methods Syst. Des. 38(1): 33-61 (2011) - [c30]Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner:
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. CPP 2011: 135-150 - [c29]Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire:
Full Reduction at Full Throttle. CPP 2011: 362-377 - [c28]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin:
Computer-Aided Security Proofs for the Working Cryptographer. CRYPTO 2011: 71-90 - [c27]Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella Béguelin:
Beyond Provable Security Verifiable IND-CCA Security of OAEP. CT-RSA 2011: 180-196 - 2010
- [c26]Gilles Barthe, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Grégoire, Sylvain Heraud:
A Machine-Checked Formalization of Sigma-Protocols. CSF 2010: 246-260 - [c25]Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry:
Extending Coq with Imperative Features and Its Application to SAT Verification. ITP 2010: 83-98 - [c24]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Programming Language Techniques for Cryptographic Proofs. ITP 2010: 115-130 - [c23]Benjamin Grégoire, Jorge Luis Sacchini:
On Strong Normalization of the Calculus of Constructions with Type-Based Termination. LPAR (Yogyakarta) 2010: 333-347
2000 – 2009
- 2009
- [j1]Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk:
Certificate translation for optimizing compilers. ACM Trans. Program. Lang. Syst. 31(5): 18:1-18:45 (2009) - [c22]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet:
Implementing a Direct Method for Certificate Translation. ICFEM 2009: 541-560 - [c21]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Formal certification of code-based cryptographic proofs. POPL 2009: 90-101 - [c20]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 - 2008
- [c19]Benjamin Grégoire, Loïc Pottier, Laurent Théry:
Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. Automated Deduction in Geometry 2008: 42-59 - [c18]Gilles Barthe, Benjamin Grégoire, Mariela Pavlova:
Preservation of Proof Obligations from Java to the Java Virtual Machine. IJCAR 2008: 83-99 - [c17]Gilles Barthe, Benjamin Grégoire, Colin Riba:
Type-Based Termination with Sized Products. CSL 2008: 493-507 - [c16]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 - [c15]Gilles Barthe, Benjamin Grégoire, Colin Riba:
A Tutorial on Type-Based Termination. LerNet ALFA Summer School 2008: 100-152 - [c14]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
- [c13]Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie:
The MOBIUS Proof Carrying Code Infrastructure. FMCO 2007: 1-24 - [c12]Benjamin Grégoire, Jorge Luis Sacchini:
Combining a Verification Condition Generator for a Bytecode Language with Static Analyses. TGC 2007: 23-40 - 2006
- [c11]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 - [c10]Benjamin Grégoire, Laurent Théry, Benjamin Werner:
A Computational Approach to Pocklington Certificates in Type Theory. FLOPS 2006: 97-113 - [c9]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 - [c8]Gilles Barthe, Benjamin Grégoire, Fernando Pastawski:
CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. LPAR 2006: 257-271 - [c7]Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk:
Certificate Translation for Optimizing Compilers. SAS 2006: 301-317 - [c6]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 - [e1]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. Lecture Notes in Computer Science 3956, Springer 2006, ISBN 3-540-33689-3 [contents] - 2005
- [c5]Bruno Barras, Benjamin Grégoire:
On the Role of Type Decorations in the Calculus of Inductive Constructions. CSL 2005: 151-166 - [c4]Gilles Barthe, Benjamin Grégoire, Fernando Pastawski:
Practical Inference for Type-Based Termination in a Polymorphic Setting. TLCA 2005: 71-85 - [c3]Benjamin Grégoire, Assia Mahboubi:
Proving Equalities in a Commutative Ring Done Right in Coq. TPHOLs 2005: 98-113 - 2004
- [c2]Yves Bertot, Benjamin Grégoire, Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES 2004: 66-81 - 2002
- [c1]Benjamin Grégoire, Xavier Leroy:
A compiled implementation of strong reduction. ICFP 2002: 235-246
Coauthor Index
[j6] [j5] [i29] [c66] [c65] [c64] [c63] [c62] [i28] [i27] [i26] [i25] [j4] [c61] [c58] [c57] [c56] [i24] [i22] [i21] [i20] [i19] [c55] [c54] [c53] [c52] [c51] [i18] [i17] [i16] [i15] [i14] [c50] [c49] [c48] [c47] [i13] [i12] [i11] [i10] [i9] [c46] [c45] [c44] [i8] [i7] [i6] [c43] [c42] [c41] [c40] [i5] [i4] [i3] [j3] [c39] [c38] [c37] [c36] [c35] [c34] [c33] [c32] [c31] [i1] [c28] [c27] [c26] [c24] [j1] [c22] [c21] [c20] [c18] [c17] [c16] [c15] [c13] [c9] [c8] [c7] [c6] [e1] [c4]
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
load content from web.archive.org
Privacy notice: By enabling the option above, your browser will contact the API of web.archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org and opencitations.net to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy.
Citation data
Add a list of citing articles from to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy.
Tweets on dblp homepage
Show tweets from 
on the dblp homepage.
Privacy notice: By enabling the option above, your browser will contact twitter.com and twimg.com to load tweets curated by our Twitter accout. At the same time, Twitter will persitently store several cookies with your web browser. While we did signal Twitter to not track our users by setting the "dnt" flag, we do not have any control over how Twitter uses your data. So please proceed with care and consider checking the Twitter privacy policy.
last updated on 2020-05-28 23:40 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
the dblp computer science bibliography is funded by:
