×
Compute Distance To:
Author ID: barthe.gilles Recent zbMATH articles by "Barthe, Gilles"
Published as: Barthe, Gilles; Barthe, G.
Homepage: https://gbarthe.github.io/
External Links: MGP · dblp
all top 5

Co-Authors

10 single-authored
27 Grégoire, Benjamin
15 Strub, Pierre-Yves
13 Hsu, Justin
11 Zanella Béguelin, Santiago
8 Kunz, César
8 Schmidt, Benedikt
7 Espitau, Thomas
7 Gaboardi, Marco
6 Dupressoir, François
6 Rezk, Tamara
5 Dufay, Guillaume
5 Hatcliff, John
5 Sørensen, Morten Heine B.
4 Crespo, Juan Manuel
4 Lakhnech, Yassine
4 Melo de Sousa, Simão
4 Olmedo, Federico
4 Pichardie, David
3 Betarte, Gustavo
3 Campo, Juan Diego
3 Coquand, Thierry
3 Fagerholm, Edvard
3 Fiore, Dario
3 Fouque, Pierre-Alain
3 Heraud, Sylvain
3 Luna, Carlos
3 Scedrov, Andre
3 Serpette, Bernard Paul
3 Silva, Alexandra
3 Tibouchi, Mehdi
2 Aguirre, Alejandro
2 Ambrona, Miguel
2 Bacelar Almeida, José
2 Baillot, Patrick
2 Barbosa, Manuel
2 Basu, Amitabh
2 Belaïd, Sonia
2 Courtieu, Pierre
2 Dal Lago, Ugo
2 D’Argenio, Pedro Rubén
2 Fournet, Cédric
2 Gallego Arias, Emilio Jesús
2 Garg, Deepak
2 Huisman, Marieke
2 Jakubiec, Line
2 Katoen, Joost-Pieter
2 Mitchell, John C.
2 Pastawski, Fernando
2 Pons, Olivier
2 Riba, Colin
2 Roth, Aaron Leon
2 Sato, Tetsuya
2 Tarento, Sabrina
1 Aldini, Alessandro
1 Barendregt, Hendrik Pieter
1 Biewer, Sebastian
1 Birkedal, Lars
1 Bizjak, Aleš
1 Buiras, Pablo
1 Capretta, Venanzio
1 Cederquist, Jan
1 Chadha, Rohit
1 Chimento, Jesús Mauricio
1 Çiçek, Ezgi
1 Cirstea, Horatiu
1 Cuellar, Jorge
1 Datta, Anupam
1 Daubignard, Marion
1 de Boer, Frank S.
1 Duclos, Mathilde
1 Dybjer, Peter
1 Etalle, Sandro
1 Faust, Sebastian
1 Ferrer Fioriti, Luis María
1 Finkbeiner, Bernd
1 Forest, Julien
1 Frade, Maria João
1 Geuvers, Jan Herman
1 Gorrieri, Roberto
1 Gurov, Dilian
1 Hermanns, Holger
1 Hermenegildo, Manuel V.
1 Hoffmann, Jan-Philipp
1 Jacomme, Charlie
1 Jagannath, Vishal
1 Kamareddine, Fairouz D.
1 Kapron, Bruce M.
1 Kirchner, Claude
1 Köpf, Boris
1 Kremer, Steve
1 Laporte, Vincent
1 Liquori, Luigi
1 Lopez, Javier
1 Melliès, Paul-André
1 Pacheco, Hugo
1 Pardo, Alberto
1 Pavlova, Mariela
1 Pereira, Vitor
1 Pinto, Linu
1 Pinto, Luís F.
...and 20 more Co-Authors

Publications by Year

Citations contained in zbMATH Open

80 Publications have been cited 379 times in 265 Documents Cited by Year
Formal certification of code-based cryptographic proofs. Zbl 1315.68081
Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago
28
2009
Setoids in type theory. Zbl 1060.03030
Barthe, Gilles; Capretta, Venanzio; Pons, Olivier
24
2003
Computer-aided security proofs for the working cryptographer. Zbl 1287.94048
Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Béguelin, Santiago Zanella
20
2011
Type-based termination of recursive definitions. Zbl 1054.68027
Barthe, G.; Frade, M. J.; Giménez, E.; Pinto, L.; Uustalu, T.
18
2004
Pure patterns type systems. Zbl 1321.68137
Barthe, Gilles; Cirstea, Horatiu; Kirchner, Claude; Liquori, Luigi
16
2003
Probabilistic relational reasoning for differential privacy. Zbl 1321.68182
Barthe, Gilles; Köpf, Boris; Olmedo, Federico; Zanella Béguelin, Santiago
13
2012
Domain-free pure type systems. Zbl 0979.03013
Barthe, Gilles; Sørensen, Morten Heine
12
2000
Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant. Zbl 1185.68616
Barthe, Gilles; Forest, Julien; Pichardie, David; Rusu, Vlad
11
2006
Parallel implementations of masking schemes and the bounded moment leakage model. Zbl 1411.94050
Barthe, Gilles; Dupressoir, François; Faust, Sebastian; Grégoire, Benjamin; Standaert, François-Xavier; Strub, Pierre-Yves
11
2017
Secure information flow by self-composition. Zbl 1252.68072
Barthe, Gilles; D’Argenio, Pedro R.; Rezk, Tamara
10
2011
Probabilistic relational verification for cryptographic implementations. Zbl 1284.68380
Barthe, Gilles; Fournet, Cédric; Grégoire, Benjamin; Strub, Pierre-Yves; Swamy, Nikhil; Zanella-Béguelin, Santiago
9
2014
Strongly-optimal structure preserving signatures from Type II pairings: synthesis and lower bounds. Zbl 1345.94036
Barthe, Gilles; Fagerholm, Edvard; Fiore, Dario; Scedrov, Andre; Schmidt, Benedikt; Tibouchi, Mehdi
8
2015
Verified proofs of higher-order masking. Zbl 1370.94486
Barthe, Gilles; Belaïd, Sonia; Dupressoir, François; Fouque, Pierre-Alain; Grégoire, Benjamin; Strub, Pierre-Yves
8
2015
Efficient reasoning about executable specifications in Coq. Zbl 1013.68539
Barthe, Gilles; Courtieu, Pierre
8
2002
CPS translations and applications: The cube and beyond. Zbl 0936.03015
Barthe, Gilles; Hatcliff, John; Sørensen, Morten Heine B.
7
1999
Certificate translation for optimizing compilers. Zbl 1225.68062
Barthe, Gilles; Grégoire, Benjamin; Kunz, César; Rezk, Tamara
7
2006
Higher-order approximate relational refinement types for mechanism design and differential privacy. Zbl 1346.68058
Barthe, Gilles; Gaboardi, Marco; Gallego Arias, Emilio Jesús; Hsu, Justin; Roth, Aaron; Strub, Pierre-Yves
7
2015
Synthesizing probabilistic invariants via Doob’s decomposition. Zbl 1411.68057
Barthe, Gilles; Espitau, Thomas; Ferrer Fioriti, Luis María; Hsu, Justin
6
2016
Proving differential privacy via probabilistic couplings. Zbl 1401.68184
Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
6
2016
Type-based termination with sized products. Zbl 1156.68341
Barthe, Gilles; Grégoire, Benjamin; Riba, Colin
6
2008
A formal executable semantics of the JavaCard platform. Zbl 0977.68577
Barthe, Gilles; Dufay, Guillaume; Jakubiec, Line; Serpette, Bernard; de Sousa, Simão Melo
6
2001
Beyond 2-safety: asymmetric product programs for relational program verification. Zbl 1419.68063
Barthe, Gilles; Crespo, Juan Manuel; Kunz, César
5
2013
Generic transformations of predicate encodings: constructions and applications. Zbl 1407.94069
Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt
5
2017
Practical inference for type-based termination in a polymorphic setting. Zbl 1114.03008
Barthe, Gilles; Grégoire, Benjamin; Pastawski, Fernando
5
2005
A certified lightweight non-interference Java bytecode verifier. Zbl 1187.68112
Barthe, Gilles; Pichardie, David; Rezk, Tamara
5
2007
A machine-checked formalization of the generic model and the random oracle model. Zbl 1126.68558
Barthe, Gilles; Cederquist, Jan; Tarento, Sabrina
5
2004
A tool-assisted framework for certified bytecode verification. Zbl 1129.68446
Barthe, Gilles; Dufay, Guillaume
5
2004
Type isomorphisms and proof reuse in dependent type theory. Zbl 0978.68044
Barthe, Gilles; Pons, Olivier
5
2001
Weak normalization implies strong normalization in a class of non-dependent pure type systems. Zbl 0983.68029
Barthe, Gilles; Hatcliff, John; Sørensen, Morten Heine
5
2001
Automated analysis of cryptographic assumptions in generic group models. Zbl 1343.94040
Barthe, Gilles; Fagerholm, Edvard; Fiore, Dario; Mitchell, John; Scedrov, Andre; Schmidt, Benedikt
4
2014
A formal correspondence between offensive and defensive JavaCard virtual machines. Zbl 1057.68571
Barthe, Gilles; Dufay, Guillaume; Jakubiec, Line; Melo de Sousa, Simão
4
2002
Product programs and relational program logics. Zbl 1355.68047
Barthe, Gilles; Crespo, Juan Manuel; Kunz, César
4
2016
EasyCrypt: a tutorial. Zbl 1448.68184
Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; Kunz, César; Schmidt, Benedikt; Strub, Pierre-Yves
3
2014
Compositional verification of secure applet interactions. Zbl 1059.68538
Barthe, Gilles; Gurov, Dilian; Huisman, Marieke
3
2002
Validation of the JavaCard platform with implicit induction techniques. Zbl 1038.68557
Barthe, Gilles; Stratulat, Sorin
3
2003
System-level non-interference of constant-time cryptography. I: Model. Zbl 1459.68026
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos
3
2019
A machine-checked formalization of the random oracle model. Zbl 1172.94560
Barthe, Gilles; Tarento, Sabrina
3
2006
Beyond differential privacy: composition theorems and relational logic for \(f\)-divergences between probabilistic programs. Zbl 1335.68043
Barthe, Gilles; Olmedo, Federico
3
2013
A two-level approach towards lean proof-checking. Zbl 1407.68431
Barthe, Gilles; Ruys, Mark; Barendregt, Henk
3
1996
Certificate translation in abstract interpretation. Zbl 1133.68315
Barthe, Gilles; Kunz, César
3
2008
CIC\(\widehat{~}\): Type-based termination of recursive definitions in the calculus of inductive constructions. Zbl 1165.03322
Barthe, Gilles; Grégoire, Benjamin; Pastawski, Fernando
3
2006
Masking the GLP lattice-based signature scheme at any order. Zbl 1428.94102
Barthe, Gilles; Belaïd, Sonia; Espitau, Thomas; Fouque, Pierre-Alain; Grégoire, Benjamin; Rossi, Mélissa; Tibouchi, Mehdi
3
2018
A program logic for union bounds. Zbl 1388.68022
Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
2
2016
Automated unbounded analysis of cryptographic constructions in the generic group model. Zbl 1371.94618
Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt
2
2016
Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. Zbl 1471.68053
Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo
2
2015
Security types preserving compilation. Zbl 1109.68025
Barthe, Gilles; Rezk, Tamara; Basu, Amitabh
2
2007
Beyond provable security verifiable IND-CCA security of OAEP. Zbl 1284.94052
Barthe, Gilles; Grégoire, Benjamin; Lakhnech, Yassine; Zanella Béguelin, Santiago
2
2011
Programming language techniques for cryptographic proofs. Zbl 1291.68323
Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago
2
2010
Mind the gap: modular machine-checked proofs of one-round key exchange protocols. Zbl 1375.94097
Barthe, Gilles; Crespo, Juan Manuel; Lakhnech, Yassine; Schmidt, Benedikt
2
2015
Type-checking injective pure type systems. Zbl 0949.03027
Barthe, Gilles
2
1999
Coupling proofs are probabilistic product programs. Zbl 1380.68267
Barthe, Gilles; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
2
2017
Security types preserving compilation. (Extended abstract). Zbl 1202.68085
Barthe, Gilles; Basu, Amitabh; Rezk, Tamara
2
2004
Verified indifferentiable hashing into elliptic curves. Zbl 1354.94021
Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Olmedo, Federico; Zanella Béguelin, Santiago
2
2012
Jakarta: A toolset for reasoning about JavaCard. Zbl 1002.68649
Barthe, G.; Dufay, G.; Huisman, M.; de Sousa, S. Melo
2
2001
Constructor subtyping in the calculus of inductive constructions. Zbl 0955.03039
Barthe, Gilles; van Raamsdonk, Femke
2
2000
A computational view of implicit coercions in type theory. Zbl 1084.68023
Barthe, Gilles
2
2005
Remarks on the equational theory of non-normalizing pure type systems. Zbl 1088.68033
Barthe, Gilles; Coquand, Thierry
2
2006
Existence and uniqueness of normal forms in pure type systems with \(\beta\eta\)-conversion. Zbl 0933.03008
Barthe, Gilles
2
1999
Domain-free pure type systems. Zbl 0887.03010
Barthe, Gilles; Sørensen, Morten Heine
2
1997
Computer-aided cryptographic proofs. Zbl 1360.94294
Barthe, Gilles; Crespo, Juan Manuel; Grégoire, Benjamin; Kunz, César; Zanella Béguelin, Santiago
2
2012
Making RSA-PSS provably secure against non-random faults. Zbl 1375.94098
Barthe, Gilles; Dupressoir, François; Fouque, Pierre-Alain; Grégoire, Benjamin; Tibouchi, Mehdi; Zapalowicz, Jean-Christophe
1
2014
On the equality of probabilistic terms. Zbl 1311.94068
Barthe, Gilles; Daubignard, Marion; Kapron, Bruce; Lakhnech, Yassine; Laporte, Vincent
1
2010
Relational cost analysis. Zbl 1380.68118
Çiçek, Ezgi; Barthe, Gilles; Gaboardi, Marco; Garg, Deepak; Hoffmann, Jan
1
2017
Formal certification of ElGamal encryption. A gentle introduction to certicrypt. Zbl 1312.94032
Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Zanella Béguelin, Santiago
1
2009
A tutorial on type-based termination. Zbl 1250.68084
Barthe, Gilles; Grégoire, Benjamin; Riba, Colin
1
2009
Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9–15, 2000. Advanced lectures. Zbl 0993.00046
1
2002
Expanding the cube. Zbl 0932.03013
Barthe, Gilles
1
1999
An introduction to dependent type theory. Zbl 1065.68025
Barthe, Gilles; Coquand, Thierry
1
2002
The relevance of proof-irrelevance. A meta-theoretical study of generalised calculi of constructions. Zbl 0914.03016
Barthe, Gilles
1
1998
Order-sorted inductive types. Zbl 0928.68022
Barthe, Gilles
1
1999
Extensions of pure type system. Zbl 1063.03508
Barthe, Gilles
1
1995
Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14–18, 2011. Proceedings. Zbl 1225.68009
1
2011
Deciding differential privacy for programs with finite inputs and outputs. Zbl 07299465
Barthe, Gilles; Chadha, Rohit; Jagannath, Vishal; Sistla, A. Prasad; Viswanathan, Mahesh
1
2020
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. Zbl 1387.94064
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Dupressoir, François
1
2016
An assertion-based program logic for probabilistic programs. Zbl 1418.68049
Barthe, Gilles; Espitau, Thomas; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
1
2018
Implicit coercions in type systems. Zbl 1434.03081
Barthe, Gilles
1
1996
Probabilistic relational Hoare logics for computer-aided security proofs. Zbl 1358.94059
Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago
1
2012
Partial evaluation and non-interference for object calculi. Zbl 0988.68049
Barthe, Gilles; Serpette, Bernard P.
1
1999
Formally verified implementation of an idealized model of virtualization. Zbl 1359.68048
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Chimento, Jesús Mauricio; Luna, Carlos
1
2014
System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory. Zbl 1459.68027
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David
1
2020
Deciding differential privacy for programs with finite inputs and outputs. Zbl 07299465
Barthe, Gilles; Chadha, Rohit; Jagannath, Vishal; Sistla, A. Prasad; Viswanathan, Mahesh
1
2020
System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory. Zbl 1459.68027
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos; Pichardie, David
1
2020
System-level non-interference of constant-time cryptography. I: Model. Zbl 1459.68026
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos
3
2019
Masking the GLP lattice-based signature scheme at any order. Zbl 1428.94102
Barthe, Gilles; Belaïd, Sonia; Espitau, Thomas; Fouque, Pierre-Alain; Grégoire, Benjamin; Rossi, Mélissa; Tibouchi, Mehdi
3
2018
An assertion-based program logic for probabilistic programs. Zbl 1418.68049
Barthe, Gilles; Espitau, Thomas; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
1
2018
Parallel implementations of masking schemes and the bounded moment leakage model. Zbl 1411.94050
Barthe, Gilles; Dupressoir, François; Faust, Sebastian; Grégoire, Benjamin; Standaert, François-Xavier; Strub, Pierre-Yves
11
2017
Generic transformations of predicate encodings: constructions and applications. Zbl 1407.94069
Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt
5
2017
Coupling proofs are probabilistic product programs. Zbl 1380.68267
Barthe, Gilles; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
2
2017
Relational cost analysis. Zbl 1380.68118
Çiçek, Ezgi; Barthe, Gilles; Gaboardi, Marco; Garg, Deepak; Hoffmann, Jan
1
2017
Synthesizing probabilistic invariants via Doob’s decomposition. Zbl 1411.68057
Barthe, Gilles; Espitau, Thomas; Ferrer Fioriti, Luis María; Hsu, Justin
6
2016
Proving differential privacy via probabilistic couplings. Zbl 1401.68184
Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
6
2016
Product programs and relational program logics. Zbl 1355.68047
Barthe, Gilles; Crespo, Juan Manuel; Kunz, César
4
2016
A program logic for union bounds. Zbl 1388.68022
Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
2
2016
Automated unbounded analysis of cryptographic constructions in the generic group model. Zbl 1371.94618
Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt
2
2016
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. Zbl 1387.94064
Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Dupressoir, François
1
2016
Strongly-optimal structure preserving signatures from Type II pairings: synthesis and lower bounds. Zbl 1345.94036
Barthe, Gilles; Fagerholm, Edvard; Fiore, Dario; Scedrov, Andre; Schmidt, Benedikt; Tibouchi, Mehdi
8
2015
Verified proofs of higher-order masking. Zbl 1370.94486
Barthe, Gilles; Belaïd, Sonia; Dupressoir, François; Fouque, Pierre-Alain; Grégoire, Benjamin; Strub, Pierre-Yves
8
2015
Higher-order approximate relational refinement types for mechanism design and differential privacy. Zbl 1346.68058
Barthe, Gilles; Gaboardi, Marco; Gallego Arias, Emilio Jesús; Hsu, Justin; Roth, Aaron; Strub, Pierre-Yves
7
2015
Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. Zbl 1471.68053
Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo
2
2015
Mind the gap: modular machine-checked proofs of one-round key exchange protocols. Zbl 1375.94097
Barthe, Gilles; Crespo, Juan Manuel; Lakhnech, Yassine; Schmidt, Benedikt
2
2015
Probabilistic relational verification for cryptographic implementations. Zbl 1284.68380
Barthe, Gilles; Fournet, Cédric; Grégoire, Benjamin; Strub, Pierre-Yves; Swamy, Nikhil; Zanella-Béguelin, Santiago
9
2014
Automated analysis of cryptographic assumptions in generic group models. Zbl 1343.94040
Barthe, Gilles; Fagerholm, Edvard; Fiore, Dario; Mitchell, John; Scedrov, Andre; Schmidt, Benedikt
4
2014
EasyCrypt: a tutorial. Zbl 1448.68184
Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; Kunz, César; Schmidt, Benedikt; Strub, Pierre-Yves
3
2014
Making RSA-PSS provably secure against non-random faults. Zbl 1375.94098
Barthe, Gilles; Dupressoir, François; Fouque, Pierre-Alain; Grégoire, Benjamin; Tibouchi, Mehdi; Zapalowicz, Jean-Christophe
1
2014
Formally verified implementation of an idealized model of virtualization. Zbl 1359.68048
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Chimento, Jesús Mauricio; Luna, Carlos
1
2014
Beyond 2-safety: asymmetric product programs for relational program verification. Zbl 1419.68063
Barthe, Gilles; Crespo, Juan Manuel; Kunz, César
5
2013
Beyond differential privacy: composition theorems and relational logic for \(f\)-divergences between probabilistic programs. Zbl 1335.68043
Barthe, Gilles; Olmedo, Federico
3
2013
Probabilistic relational reasoning for differential privacy. Zbl 1321.68182
Barthe, Gilles; Köpf, Boris; Olmedo, Federico; Zanella Béguelin, Santiago
13
2012
Verified indifferentiable hashing into elliptic curves. Zbl 1354.94021
Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Olmedo, Federico; Zanella Béguelin, Santiago
2
2012
Computer-aided cryptographic proofs. Zbl 1360.94294
Barthe, Gilles; Crespo, Juan Manuel; Grégoire, Benjamin; Kunz, César; Zanella Béguelin, Santiago
2
2012
Probabilistic relational Hoare logics for computer-aided security proofs. Zbl 1358.94059
Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago
1
2012
Computer-aided security proofs for the working cryptographer. Zbl 1287.94048
Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Béguelin, Santiago Zanella
20
2011
Secure information flow by self-composition. Zbl 1252.68072
Barthe, Gilles; D’Argenio, Pedro R.; Rezk, Tamara
10
2011
Beyond provable security verifiable IND-CCA security of OAEP. Zbl 1284.94052
Barthe, Gilles; Grégoire, Benjamin; Lakhnech, Yassine; Zanella Béguelin, Santiago
2
2011
Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14–18, 2011. Proceedings. Zbl 1225.68009
1
2011
Programming language techniques for cryptographic proofs. Zbl 1291.68323
Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago
2
2010
On the equality of probabilistic terms. Zbl 1311.94068
Barthe, Gilles; Daubignard, Marion; Kapron, Bruce; Lakhnech, Yassine; Laporte, Vincent
1
2010
Formal certification of code-based cryptographic proofs. Zbl 1315.68081
Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago
28
2009
Formal certification of ElGamal encryption. A gentle introduction to certicrypt. Zbl 1312.94032
Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Zanella Béguelin, Santiago
1
2009
A tutorial on type-based termination. Zbl 1250.68084
Barthe, Gilles; Grégoire, Benjamin; Riba, Colin
1
2009
Type-based termination with sized products. Zbl 1156.68341
Barthe, Gilles; Grégoire, Benjamin; Riba, Colin
6
2008
Certificate translation in abstract interpretation. Zbl 1133.68315
Barthe, Gilles; Kunz, César
3
2008
A certified lightweight non-interference Java bytecode verifier. Zbl 1187.68112
Barthe, Gilles; Pichardie, David; Rezk, Tamara
5
2007
Security types preserving compilation. Zbl 1109.68025
Barthe, Gilles; Rezk, Tamara; Basu, Amitabh
2
2007
Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant. Zbl 1185.68616
Barthe, Gilles; Forest, Julien; Pichardie, David; Rusu, Vlad
11
2006
Certificate translation for optimizing compilers. Zbl 1225.68062
Barthe, Gilles; Grégoire, Benjamin; Kunz, César; Rezk, Tamara
7
2006
A machine-checked formalization of the random oracle model. Zbl 1172.94560
Barthe, Gilles; Tarento, Sabrina
3
2006
CIC\(\widehat{~}\): Type-based termination of recursive definitions in the calculus of inductive constructions. Zbl 1165.03322
Barthe, Gilles; Grégoire, Benjamin; Pastawski, Fernando
3
2006
Remarks on the equational theory of non-normalizing pure type systems. Zbl 1088.68033
Barthe, Gilles; Coquand, Thierry
2
2006
Practical inference for type-based termination in a polymorphic setting. Zbl 1114.03008
Barthe, Gilles; Grégoire, Benjamin; Pastawski, Fernando
5
2005
A computational view of implicit coercions in type theory. Zbl 1084.68023
Barthe, Gilles
2
2005
Type-based termination of recursive definitions. Zbl 1054.68027
Barthe, G.; Frade, M. J.; Giménez, E.; Pinto, L.; Uustalu, T.
18
2004
A machine-checked formalization of the generic model and the random oracle model. Zbl 1126.68558
Barthe, Gilles; Cederquist, Jan; Tarento, Sabrina
5
2004
A tool-assisted framework for certified bytecode verification. Zbl 1129.68446
Barthe, Gilles; Dufay, Guillaume
5
2004
Security types preserving compilation. (Extended abstract). Zbl 1202.68085
Barthe, Gilles; Basu, Amitabh; Rezk, Tamara
2
2004
Setoids in type theory. Zbl 1060.03030
Barthe, Gilles; Capretta, Venanzio; Pons, Olivier
24
2003
Pure patterns type systems. Zbl 1321.68137
Barthe, Gilles; Cirstea, Horatiu; Kirchner, Claude; Liquori, Luigi
16
2003
Validation of the JavaCard platform with implicit induction techniques. Zbl 1038.68557
Barthe, Gilles; Stratulat, Sorin
3
2003
Efficient reasoning about executable specifications in Coq. Zbl 1013.68539
Barthe, Gilles; Courtieu, Pierre
8
2002
A formal correspondence between offensive and defensive JavaCard virtual machines. Zbl 1057.68571
Barthe, Gilles; Dufay, Guillaume; Jakubiec, Line; Melo de Sousa, Simão
4
2002
Compositional verification of secure applet interactions. Zbl 1059.68538
Barthe, Gilles; Gurov, Dilian; Huisman, Marieke
3
2002
Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9–15, 2000. Advanced lectures. Zbl 0993.00046
1
2002
An introduction to dependent type theory. Zbl 1065.68025
Barthe, Gilles; Coquand, Thierry
1
2002
A formal executable semantics of the JavaCard platform. Zbl 0977.68577
Barthe, Gilles; Dufay, Guillaume; Jakubiec, Line; Serpette, Bernard; de Sousa, Simão Melo
6
2001
Type isomorphisms and proof reuse in dependent type theory. Zbl 0978.68044
Barthe, Gilles; Pons, Olivier
5
2001
Weak normalization implies strong normalization in a class of non-dependent pure type systems. Zbl 0983.68029
Barthe, Gilles; Hatcliff, John; Sørensen, Morten Heine
5
2001
Jakarta: A toolset for reasoning about JavaCard. Zbl 1002.68649
Barthe, G.; Dufay, G.; Huisman, M.; de Sousa, S. Melo
2
2001
Domain-free pure type systems. Zbl 0979.03013
Barthe, Gilles; Sørensen, Morten Heine
12
2000
Constructor subtyping in the calculus of inductive constructions. Zbl 0955.03039
Barthe, Gilles; van Raamsdonk, Femke
2
2000
CPS translations and applications: The cube and beyond. Zbl 0936.03015
Barthe, Gilles; Hatcliff, John; Sørensen, Morten Heine B.
7
1999
Type-checking injective pure type systems. Zbl 0949.03027
Barthe, Gilles
2
1999
Existence and uniqueness of normal forms in pure type systems with \(\beta\eta\)-conversion. Zbl 0933.03008
Barthe, Gilles
2
1999
Expanding the cube. Zbl 0932.03013
Barthe, Gilles
1
1999
Order-sorted inductive types. Zbl 0928.68022
Barthe, Gilles
1
1999
Partial evaluation and non-interference for object calculi. Zbl 0988.68049
Barthe, Gilles; Serpette, Bernard P.
1
1999
The relevance of proof-irrelevance. A meta-theoretical study of generalised calculi of constructions. Zbl 0914.03016
Barthe, Gilles
1
1998
Domain-free pure type systems. Zbl 0887.03010
Barthe, Gilles; Sørensen, Morten Heine
2
1997
A two-level approach towards lean proof-checking. Zbl 1407.68431
Barthe, Gilles; Ruys, Mark; Barendregt, Henk
3
1996
Implicit coercions in type systems. Zbl 1434.03081
Barthe, Gilles
1
1996
Extensions of pure type system. Zbl 1063.03508
Barthe, Gilles
1
1995
all top 5

Cited by 483 Authors

22 Barthe, Gilles
8 Abel, Andreas M.
7 Kirchner, Claude
5 Cirstea, Horatiu
5 Fujita, Ken-etsu
5 Grégoire, Benjamin
5 Kunz, César
5 Lakhnech, Yassine
5 Maietti, Maria Emilia
5 Pichardie, David
5 Sørensen, Morten Heine B.
4 Blanqui, Frédéric
4 Gaboardi, Marco
4 Nowak, David E.
4 Strub, Pierre-Yves
3 Beringer, Lennart
3 Bertolissi, Clara
3 Bertot, Yves
3 Crespo, Juan Manuel
3 Dal Lago, Ugo
3 Dupressoir, François
3 Ene, Cristian
3 Faure, Germain
3 Fiore, Dario
3 Guilley, Sylvain
3 Hatcliff, John
3 Jacobs, Bart
3 Kaminski, Benjamin Lucien
3 Katoen, Joost-Pieter
3 Krauss, Alexander
3 Lafourcade, Pascal
3 Lochbihler, Andreas
3 Melo de Sousa, Simão
3 Rivain, Matthieu
3 Rosolini, Giuseppe
3 Sato, Tetsuya
3 Schubert, Aleksy
3 Standaert, Francois-Xavier
3 Stratulat, Sorin
3 Stump, Aaron
3 Tibouchi, Mehdi
3 Uustalu, Tarmo
3 Zhang, Yu
2 Abe, Masayuki
2 Affeldt, Reynald
2 Allamigeon, Xavier
2 Asperti, Andrea
2 Ayala-Rincón, Mauricio
2 Bacelar Almeida, José
2 Baillot, Patrick
2 Barbosa, Manuel
2 Bartocci, Ezio
2 Betarte, Gustavo
2 Blanchette, Jasmin Christian
2 Bove, Ana
2 Cachera, David
2 Campo, Juan Diego
2 Courant, Judicaël
2 Damgård, Ivan Bjerre
2 Danger, Jean-Luc
2 D’Argenio, Pedro Rubén
2 Daubignard, Marion
2 Fallah, Mehran S.
2 Faust, Sebastian
2 Fernández, Maribel
2 Finkbeiner, Bernd
2 Fuchsbauer, Georg
2 Fuhs, Carsten
2 Gonthier, Georges
2 Goudarzi, Dahmun
2 Gurov, Dilian
2 Hanser, Christian
2 Harper, Robert
2 Hofmann, Martin
2 Hsu, Justin
2 Huisman, Marieke
2 Klebanov, Vladimir
2 Klein, Gerwin
2 Kohlweiss, Markulf
2 Komendantskaya, Ekaterina
2 Kovács, Laura Ildikó
2 Leroy, Xavier
2 Liquori, Luigi
2 Luna, Carlos
2 Mahboubi, Assia
2 Matthes, Ralph
2 Moreira, Nelma
2 Nakazawa, Koji
2 Nipkow, Tobias
2 Ohkubo, Miyako
2 Olmedo, Federico
2 Orchard, Dominic A.
2 Orlandi, Claudio
2 Pagano, Miguel
2 Palamidessi, Catuscia
2 Pereira, David P.
2 Petit, Barbara
2 Pinto, Jorge Sousa
2 Reps, Thomas W.
2 Rezk, Tamara
...and 383 more Authors

Citations by Year