×

zbMATH — the first resource for mathematics

Barthe, Gilles

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
Documents Indexed: 119 Publications since 1995, including 11 Books
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 Baillot, Patrick
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 Bacelar Almeida, José
1 Barbosa, Manuel
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 Pardo, Alberto
1 Pavlova, Mariela
1 Pinto, L.
1 Pinto, Luís F.
1 Pretschner, Alexander
1 Ríos, Alejandro
...and 17 more Co-Authors

Publications by Year

Citations contained in zbMATH Open

72 Publications have been cited 326 times in 227 Documents Cited by Year
Formal certification of code-based cryptographic proofs. Zbl 1315.68081
Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago
26
2009
Setoids in type theory. Zbl 1060.03030
Barthe, Gilles; Capretta, Venanzio; Pons, Olivier
23
2003
Type-based termination of recursive definitions. Zbl 1054.68027
Barthe, G.; Frade, M. J.; Giménez, E.; Pinto, L.; Uustalu, T.
17
2004
Computer-aided security proofs for the working cryptographer. Zbl 1287.94048
Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Béguelin, Santiago Zanella
17
2011
Pure patterns type systems. Zbl 1321.68137
Barthe, Gilles; Cirstea, Horatiu; Kirchner, Claude; Liquori, Luigi
16
2003
Domain-free pure type systems. Zbl 0979.03013
Barthe, Gilles; Sørensen, Morten Heine
11
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
10
2006
Probabilistic relational reasoning for differential privacy. Zbl 1321.68182
Barthe, Gilles; Köpf, Boris; Olmedo, Federico; Zanella Béguelin, Santiago
9
2012
Efficient reasoning about executable specifications in Coq. Zbl 1013.68539
Barthe, Gilles; Courtieu, Pierre
8
2002
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
8
2014
Certificate translation for optimizing compilers. Zbl 1225.68062
Barthe, Gilles; Grégoire, Benjamin; Kunz, César; Rezk, Tamara
7
2006
Secure information flow by self-composition. Zbl 1252.68072
Barthe, Gilles; D’Argenio, Pedro R.; Rezk, Tamara
7
2011
CPS translations and applications: The cube and beyond. Zbl 0936.03015
Barthe, Gilles; Hatcliff, John; Sørensen, Morten Heine B.
7
1999
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
7
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
7
2015
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
7
2017
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-based termination with sized products. Zbl 1156.68341
Barthe, Gilles; Grégoire, Benjamin; Riba, Colin
6
2008
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
A certified lightweight non-interference Java bytecode verifier. Zbl 1187.68112
Barthe, Gilles; Pichardie, David; Rezk, Tamara
5
2007
A tool-assisted framework for certified bytecode verification. Zbl 1129.68446
Barthe, Gilles; Dufay, Guillaume
5
2004
Practical inference for type-based termination in a polymorphic setting. Zbl 1114.03008
Barthe, Gilles; Grégoire, Benjamin; Pastawski, Fernando
5
2005
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 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
Beyond 2-safety: asymmetric product programs for relational program verification. Zbl 1419.68063
Barthe, Gilles; Crespo, Juan Manuel; Kunz, César
4
2013
Proving differential privacy via probabilistic couplings. Zbl 1401.68184
Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
4
2016
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
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
4
2015
Synthesizing probabilistic invariants via Doob’s decomposition. Zbl 1411.68057
Barthe, Gilles; Espitau, Thomas; Ferrer Fioriti, Luis María; Hsu, Justin
3
2016
Validation of the JavaCard platform with implicit induction techniques. Zbl 1038.68557
Barthe, Gilles; Stratulat, Sorin
3
2003
Compositional verification of secure applet interactions. Zbl 1059.68538
Barthe, Gilles; Gurov, Dilian; Huisman, Marieke
3
2002
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
A machine-checked formalization of the random oracle model. Zbl 1172.94560
Barthe, Gilles; Tarento, Sabrina
3
2006
A two-level approach towards lean proof-checking. Zbl 1407.68431
Barthe, Gilles; Ruys, Mark; Barendregt, Henk
3
1996
Beyond differential privacy: composition theorems and relational logic for \(f\)-divergences between probabilistic programs. Zbl 1335.68043
Barthe, Gilles; Olmedo, Federico
3
2013
EasyCrypt: a tutorial. Zbl 1448.68184
Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; Kunz, César; Schmidt, Benedikt; Strub, Pierre-Yves
3
2014
Domain-free pure type systems. Zbl 0887.03010
Barthe, Gilles; Sørensen, Morten Heine
2
1997
Programming language techniques for cryptographic proofs. Zbl 1291.68323
Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago
2
2010
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
A computational view of implicit coercions in type theory. Zbl 1084.68023
Barthe, Gilles
2
2005
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
System-level non-interference of constant-time cryptography. I: Model. Zbl 1459.68026
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos
2
2019
Existence and uniqueness of normal forms in pure type systems with \(\beta\eta\)-conversion. Zbl 0933.03008
Barthe, Gilles
2
1999
Constructor subtyping in the calculus of inductive constructions. Zbl 0955.03039
Barthe, Gilles; van Raamsdonk, Femke
2
2000
Type-checking injective pure type systems. Zbl 0949.03027
Barthe, Gilles
2
1999
Remarks on the equational theory of non-normalizing pure type systems. Zbl 1088.68033
Barthe, Gilles; Coquand, Thierry
2
2006
Generic transformations of predicate encodings: constructions and applications. Zbl 1407.94069
Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt
2
2017
Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. Zbl 06528783
Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo
2
2015
Product programs and relational program logics. Zbl 1355.68047
Barthe, Gilles; Crespo, Juan Manuel; Kunz, César
2
2016
Jakarta: A toolset for reasoning about JavaCard. Zbl 1002.68649
Barthe, G.; Dufay, G.; Huisman, M.; de Sousa, S. Melo
2
2001
A tutorial on type-based termination. Zbl 1250.68084
Barthe, Gilles; Grégoire, Benjamin; Riba, Colin
2
2009
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
Order-sorted inductive types. Zbl 0928.68022
Barthe, Gilles
1
1999
Expanding the cube. Zbl 0932.03013
Barthe, Gilles
1
1999
Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9–15, 2000. Advanced lectures. Zbl 0993.00046
Barthe, Gilles (ed.); Dybjer, Peter (ed.); Pinto, Luís (ed.); Saraiva, João (ed.)
1
2002
An introduction to dependent type theory. Zbl 1065.68025
Barthe, Gilles; Coquand, Thierry
1
2002
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
Security types preserving compilation. Zbl 1109.68025
Barthe, Gilles; Rezk, Tamara; Basu, Amitabh
1
2007
Probabilistic relational Hoare logics for computer-aided security proofs. Zbl 1358.94059
Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago
1
2012
Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14–18, 2011. Proceedings. Zbl 1225.68009
Barthe, Gilles (ed.); Pardo, Alberto (ed.); Schneider, Gerardo (ed.)
1
2011
Implicit coercions in type systems. Zbl 1434.03081
Barthe, Gilles
1
1996
Extensions of pure type system. Zbl 1063.03508
Barthe, Gilles
1
1995
On the equality of probabilistic terms. Zbl 1311.94068
Barthe, Gilles; Daubignard, Marion; Kapron, Bruce; Lakhnech, Yassine; Laporte, Vincent
1
2010
Coupling proofs are probabilistic product programs. Zbl 1380.68267
Barthe, Gilles; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
1
2017
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
Automated unbounded analysis of cryptographic constructions in the generic group model. Zbl 1371.94618
Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt
1
2016
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
Security types preserving compilation. (Extended abstract). Zbl 1202.68085
Barthe, Gilles; Basu, Amitabh; Rezk, Tamara
1
2004
System-level non-interference of constant-time cryptography. I: Model. Zbl 1459.68026
Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos
2
2019
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
7
2017
Generic transformations of predicate encodings: constructions and applications. Zbl 1407.94069
Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt
2
2017
Coupling proofs are probabilistic product programs. Zbl 1380.68267
Barthe, Gilles; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
1
2017
Proving differential privacy via probabilistic couplings. Zbl 1401.68184
Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves
4
2016
Synthesizing probabilistic invariants via Doob’s decomposition. Zbl 1411.68057
Barthe, Gilles; Espitau, Thomas; Ferrer Fioriti, Luis María; Hsu, Justin
3
2016
Product programs and relational program logics. Zbl 1355.68047
Barthe, Gilles; Crespo, Juan Manuel; Kunz, César
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
Automated unbounded analysis of cryptographic constructions in the generic group model. Zbl 1371.94618
Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt
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
7
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
7
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
4
2015
Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. Zbl 06528783
Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo
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
8
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
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
4
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
9
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
17
2011
Secure information flow by self-composition. Zbl 1252.68072
Barthe, Gilles; D’Argenio, Pedro R.; Rezk, Tamara
7
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
Barthe, Gilles; Pardo, Alberto; Schneider, Gerardo
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
26
2009
A tutorial on type-based termination. Zbl 1250.68084
Barthe, Gilles; Grégoire, Benjamin; Riba, Colin
2
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
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
1
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
10
2006
Certificate translation for optimizing compilers. Zbl 1225.68062
Barthe, Gilles; Grégoire, Benjamin; Kunz, César; Rezk, Tamara
7
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
A machine-checked formalization of the random oracle model. Zbl 1172.94560
Barthe, Gilles; Tarento, Sabrina
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.
17
2004
A tool-assisted framework for certified bytecode verification. Zbl 1129.68446
Barthe, Gilles; Dufay, Guillaume
5
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
Security types preserving compilation. (Extended abstract). Zbl 1202.68085
Barthe, Gilles; Basu, Amitabh; Rezk, Tamara
1
2004
Setoids in type theory. Zbl 1060.03030
Barthe, Gilles; Capretta, Venanzio; Pons, Olivier
23
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
Barthe, Gilles; Dybjer, Peter; Pinto, Luís; Saraiva, João
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
11
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
Existence and uniqueness of normal forms in pure type systems with \(\beta\eta\)-conversion. Zbl 0933.03008
Barthe, Gilles
2
1999
Type-checking injective pure type systems. Zbl 0949.03027
Barthe, Gilles
2
1999
Partial evaluation and non-interference for object calculi. Zbl 0988.68049
Barthe, Gilles; Serpette, Bernard P.
1
1999
Order-sorted inductive types. Zbl 0928.68022
Barthe, Gilles
1
1999
Expanding the cube. Zbl 0932.03013
Barthe, Gilles
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 388 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 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 Hatcliff, John
3 Jacobs, Bart
3 Krauss, Alexander
3 Lafourcade, Pascal
3 Lochbihler, Andreas
3 Melo de Sousa, Simão
3 Rosolini, Giuseppe
3 Schubert, Aleksy
3 Standaert, Francois-Xavier
3 Stratulat, Sorin
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 Betarte, Gustavo
2 Blanchette, Jasmin Christian
2 Bove, Ana
2 Cachera, David
2 Campo, Juan Diego
2 Courant, Judicaël
2 D’Argenio, Pedro Rubén
2 Daubignard, Marion
2 Fallah, Mehran S.
2 Faust, Sebastian
2 Fernández, Maribel
2 Fiore, Dario
2 Fuchsbauer, Georg
2 Fuhs, Carsten
2 Gonthier, Georges
2 Goudarzi, Dahmun
2 Guilley, Sylvain
2 Gurov, Dilian
2 Hanser, Christian
2 Harper, Robert
2 Hofmann, Martin
2 Hsu, Justin
2 Huisman, Marieke
2 Kaminski, Benjamin Lucien
2 Katoen, Joost-Pieter
2 Klebanov, Vladimir
2 Klein, Gerwin
2 Komendantskaya, Ekaterina
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 Pagano, Miguel
2 Palamidessi, Catuscia
2 Pereira, David P.
2 Petit, Barbara
2 Pinto, Jorge Sousa
2 Rezk, Tamara
2 Riba, Colin
2 Rideau, Laurence
2 Rivain, Matthieu
2 Saabas, Ando
2 Sato, Tetsuya
2 Schmidt, Benedikt
2 Seldin, Jonathan P.
2 Slamanig, Daniel
2 Spitters, Bas
2 Stump, Aaron
2 Tassi, Enrico
2 Thiemann, René
2 Ulbrich, Mattias
2 Villar, Jorge Luis
...and 288 more Authors

Citations by Year