Edit Profile (opens in new tab) Barthe, Gilles Co-Author Distance Author ID: barthe.gilles Published as: Barthe, Gilles; Barthe, G. Homepage: https://gbarthe.github.io/ External Links: MGP · dblp Documents Indexed: 117 Publications since 1995, including 1 Additional arXiv Preprint 12 Contributions as Editor Software Indexed: 6 Packages Co-Authors: 134 Co-Authors with 117 Joint Publications 2,730 Co-Co-Authors all top 5 Co-Authors 11 single-authored 29 Grégoire, Benjamin 15 Strub, Pierre-Yves 13 Hsu, Justin 11 Zanella Béguelin, Santiago 8 Espitau, Thomas 8 Gaboardi, Marco 8 Kunz, César 8 Schmidt, Benedikt 6 Dupressoir, François 6 Rezk, Tamara 5 Dufay, Guillaume 5 Hatcliff, John 5 Pichardie, David 5 Sørensen, Morten Heine B. 4 Barbosa, Manuel 4 Crespo, Juan Manuel 4 Fouque, Pierre-Alain 4 Lakhnech, Yassine 4 Melo de Sousa, Simão 4 Olmedo, Federico 4 Tibouchi, Mehdi 3 Bacelar Almeida, José 3 Belaïd, Sonia 3 Betarte, Gustavo 3 Campo, Juan Diego 3 Coquand, Thierry 3 Dal Lago, Ugo 3 Fagerholm, Edvard 3 Fiore, Dario 3 Heraud, Sylvain 3 Luna, Carlos 3 Ščedrov, Andrej 3 Serpette, Bernard Paul 3 Silva, Alexandra 2 Aguirre, Alejandro 2 Ambrona, Miguel 2 Baillot, Patrick 2 Basu, Amitabh 2 Courtieu, Pierre 2 D’Argenio, Pedro Rubén 2 Fournet, Cédric 2 Gallego Arias, Emilio Jesús 2 Garg, Deepak 2 Geuvers, Jan Herman 2 Huisman, Marieke 2 Jacomme, Charlie 2 Jakubiec, Line 2 Katoen, Joost-Pieter 2 Kremer, Steve 2 Laporte, Vincent 2 Mitchell, John C. 2 Pastawski, Fernando 2 Pons, Olivier 2 Riba, Colin 2 Rossi, Mélissa 2 Roth, Aaron Leon 2 Sato, Tetsuya 2 Tarento, Sabrina 1 Aldini, Alessandro 1 Balle, Borja 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 Crubillé, Raphaëlle 1 Cuellar, Jorge 1 Datta, Anupam 1 Daubignard, Marion 1 de Boer, Frank S. 1 Doczkal, Christian 1 Don, Jelle 1 Duclos, Mathilde 1 Dybjer, Peter 1 Etalle, Sandro 1 Faust, Sebastian 1 Fehr, Serge 1 Ferrer Fioriti, Luis María 1 Finkbeiner, Bernd 1 Forest, Julien 1 Frade, Maria João 1 Gavazzo, Francesco 1 Geumlek, Joseph 1 Gorrieri, Roberto 1 Gurov, Dilian 1 Hermanns, Holger 1 Hermenegildo, Manuel V. 1 Hoffmann, Jan-Philipp 1 Huang, Yu-Hsuan 1 Hülsing, Andreas 1 Jagannath, Vishal 1 Kamareddine, Fairouz D. 1 Kapron, Bruce M. 1 Kirchner, Claude ...and 34 more Co-Authors all top 5 Serials 9 Lecture Notes in Computer Science 5 Journal of Functional Programming 4 Journal of Automated Reasoning 4 Mathematical Structures in Computer Science 2 Theoretical Computer Science 2 Journal of Cryptology 2 Journal of Logical and Algebraic Methods in Programming 1 Information and Computation 1 Higher-Order and Symbolic Computation 1 Computer Languages, Systems & Structures 1 ACM Transactions on Computational Logic 1 Logical Methods in Computer Science 1 EPiC Series in Computing all top 5 Fields 101 Computer science (68-XX) 43 Mathematical logic and foundations (03-XX) 41 Information and communication theory, circuits (94-XX) 11 General and overarching topics; collections (00-XX) 3 Number theory (11-XX) 2 Probability theory and stochastic processes (60-XX) 2 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 1 General algebraic systems (08-XX) Publications by Year all cited Publications top 5 cited Publications Citations contained in zbMATH Open 96 Publications have been cited 719 times in 485 Documents Cited by ▼ Year ▼ Formal certification of code-based cryptographic proofs. Zbl 1315.68081 Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago 49 2009 Setoids in type theory. Zbl 1060.03030 Barthe, Gilles; Capretta, Venanzio; Pons, Olivier 33 2003 Secure information flow by self-composition. Zbl 1252.68072 Barthe, Gilles; D’Argenio, Pedro R.; Rezk, Tamara 32 2011 Probabilistic relational reasoning for differential privacy. Zbl 1321.68182 Barthe, Gilles; Köpf, Boris; Olmedo, Federico; Zanella Béguelin, Santiago 31 2012 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 27 2015 Type-based termination of recursive definitions. Zbl 1054.68027 Barthe, G.; Frade, M. J.; Giménez, E.; Pinto, L.; Uustalu, T. 27 2004 Computer-aided security proofs for the working cryptographer. Zbl 1287.94048 Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Béguelin, Santiago Zanella 25 2011 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 24 2017 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 18 2018 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 18 2014 Generic transformations of predicate encodings: constructions and applications. Zbl 1407.94069 Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt 18 2017 Proving differential privacy via probabilistic couplings. Zbl 1401.68184 Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves 17 2016 Pure patterns type systems. Zbl 1321.68137 Barthe, Gilles; Cirstea, Horatiu; Kirchner, Claude; Liquori, Luigi 16 2003 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 16 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 15 2015 Synthesizing probabilistic invariants via Doob’s decomposition. Zbl 1411.68057 Barthe, Gilles; Espitau, Thomas; Ferrer Fioriti, Luis María; Hsu, Justin 15 2016 Domain-free pure type systems. Zbl 0979.03013 Barthe, Gilles; Sørensen, Morten Heine 13 2000 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 11 2015 Automated analysis of cryptographic assumptions in generic group models. Zbl 1343.94040 Barthe, Gilles; Fagerholm, Edvard; Fiore, Dario; Mitchell, John; Scedrov, Andre; Schmidt, Benedikt 11 2014 Beyond 2-safety: asymmetric product programs for relational program verification. Zbl 1419.68063 Barthe, Gilles; Crespo, Juan Manuel; Kunz, César 11 2013 CPS translations and applications: The cube and beyond. Zbl 0936.03015 Barthe, Gilles; Hatcliff, John; Sørensen, Morten Heine B. 10 1999 Certificate translation for optimizing compilers. Zbl 1225.68062 Barthe, Gilles; Grégoire, Benjamin; Kunz, César; Rezk, Tamara 10 2006 Type-based termination with sized products. Zbl 1156.68341 Barthe, Gilles; Grégoire, Benjamin; Riba, Colin 10 2008 EasyCrypt: a tutorial. Zbl 1448.68184 Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; Kunz, César; Schmidt, Benedikt; Strub, Pierre-Yves 9 2014 Type isomorphisms and proof reuse in dependent type theory. Zbl 0978.68044 Barthe, Gilles; Pons, Olivier 9 2001 On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem. Zbl 1508.68055 Barthe, Gilles; Crubillé, Raphaëlle; Dal Lago, Ugo; Gavazzo, Francesco 9 2020 A certified lightweight non-interference Java bytecode verifier. Zbl 1187.68112 Barthe, Gilles; Pichardie, David; Rezk, Tamara 8 2007 Efficient reasoning about executable specifications in Coq. Zbl 1013.68539 Barthe, Gilles; Courtieu, Pierre 8 2002 Beyond differential privacy: composition theorems and relational logic for \(f\)-divergences between probabilistic programs. Zbl 1335.68043 Barthe, Gilles; Olmedo, Federico 8 2013 A formal executable semantics of the JavaCard platform. Zbl 0977.68577 Barthe, Gilles; Dufay, Guillaume; Jakubiec, Line; Serpette, Bernard; de Sousa, Simão Melo 7 2001 Practical inference for type-based termination in a polymorphic setting. Zbl 1114.03008 Barthe, Gilles; Grégoire, Benjamin; Pastawski, Fernando 7 2005 A machine-checked formalization of the generic model and the random oracle model. Zbl 1126.68558 Barthe, Gilles; Cederquist, Jan; Tarento, Sabrina 7 2004 Formal methods for open object-based distributed systems. 10th IFIP WG 6.1 international conference, FMOODS 2008, Oslo, Norway, June 4–6, 2008. Proceedings. Zbl 1137.68301 7 2008 Automated unbounded analysis of cryptographic constructions in the generic group model. Zbl 1371.94618 Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt 6 2016 Deciding differential privacy for programs with finite inputs and outputs. Zbl 1507.68111 Barthe, Gilles; Chadha, Rohit; Jagannath, Vishal; Sistla, A. Prasad; Viswanathan, Mahesh 6 2020 Product programs and relational program logics. Zbl 1355.68047 Barthe, Gilles; Crespo, Juan Manuel; Kunz, César 6 2016 CIC\(\widehat{~}\): Type-based termination of recursive definitions in the calculus of inductive constructions. Zbl 1165.03322 Barthe, Gilles; Grégoire, Benjamin; Pastawski, Fernando 6 2006 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 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 5 2020 Beyond provable security verifiable IND-CCA security of OAEP. Zbl 1284.94052 Barthe, Gilles; Grégoire, Benjamin; Lakhnech, Yassine; Zanella Béguelin, Santiago 5 2011 A tool-assisted framework for certified bytecode verification. Zbl 1129.68446 Barthe, Gilles; Dufay, Guillaume 5 2004 Relational cost analysis. Zbl 1380.68118 Çiçek, Ezgi; Barthe, Gilles; Gaboardi, Marco; Garg, Deepak; Hoffmann, Jan 5 2017 Implicit coercions in type systems. Zbl 1434.03081 Barthe, Gilles 5 1996 A two-level approach towards lean proof-checking. Zbl 1407.68431 Barthe, Gilles; Ruys, Mark; Barendregt, Henk 5 1996 Computer-aided cryptographic proofs. Zbl 1360.94294 Barthe, Gilles; Crespo, Juan Manuel; Grégoire, Benjamin; Kunz, César; Zanella Béguelin, Santiago 5 2012 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 4 2015 Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. Zbl 1471.68053 Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo 4 2015 Type-checking injective pure type systems. Zbl 0949.03027 Barthe, Gilles 4 1999 Foundations of probabilistic programming. Zbl 1458.68003 4 2021 Coupling proofs are probabilistic product programs. Zbl 1380.68267 Barthe, Gilles; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves 4 2017 Validation of the JavaCard platform with implicit induction techniques. Zbl 1038.68557 Barthe, Gilles; Stratulat, Sorin 4 2003 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 Certificate translation in abstract interpretation. Zbl 1133.68315 Barthe, Gilles; Kunz, César 4 2008 Relational reasoning via probabilistic coupling. Zbl 1471.68127 Barthe, Gilles; Espitau, Thomas; Grégoire, Benjamin; Hsu, Justin; Stefanesco, Léo; Strub, Pierre-Yves 3 2015 Is your software on dope? Formal analysis of surreptitiously “enhanced” programs. Zbl 1485.68059 D’Argenio, Pedro R.; Barthe, Gilles; Biewer, Sebastian; Finkbeiner, Bernd; Hermanns, Holger 3 2017 Existence and uniqueness of normal forms in pure type systems with \(\beta\eta\)-conversion. Zbl 0933.03008 Barthe, Gilles 3 1999 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 3 2014 Universal equivalence and majority of probabilistic programs over finite fields. Zbl 1496.68186 Barthe, Gilles; Jacomme, Charlie; Kremer, Steve 3 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 A machine-checked formalization of the random oracle model. Zbl 1172.94560 Barthe, Gilles; Tarento, Sabrina 3 2006 Security types preserving compilation. Zbl 1109.68025 Barthe, Gilles; Rezk, Tamara; Basu, Amitabh 3 2007 An introduction to dependent type theory. Zbl 1065.68025 Barthe, Gilles; Coquand, Thierry 3 2002 Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. Zbl 1387.94064 Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles; Dupressoir, François 3 2016 A program logic for union bounds. Zbl 1388.68022 Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves 3 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 3 2018 A tutorial on type-based termination. Zbl 1250.68084 Barthe, Gilles; Grégoire, Benjamin; Riba, Colin 3 2009 Jakarta: A toolset for reasoning about JavaCard. Zbl 1002.68649 Barthe, G.; Dufay, G.; Huisman, M.; de Sousa, S. Melo 3 2001 Compositional verification of secure applet interactions. Zbl 1059.68538 Barthe, Gilles; Gurov, Dilian; Huisman, Marieke 3 2002 Partial evaluation and non-interference for object calculi. Zbl 0988.68049 Barthe, Gilles; Serpette, Bernard P. 2 1999 Extensions of pure type system. Zbl 1063.03508 Barthe, Gilles 2 1995 Domain-free pure type systems. Zbl 0887.03010 Barthe, Gilles; Sørensen, Morten Heine 2 1997 A notion of classical pure type system. Zbl 0911.68109 Barthe, Gilles; Hatcliff, John; Sørenson, Morten 2 1997 Constructor subtyping in the calculus of inductive constructions. Zbl 0955.03039 Barthe, Gilles; van Raamsdonk, Femke 2 2000 \(*\)-liftings for differential privacy. Zbl 1442.68100 Barthe, Gilles; Espitau, Thomas; Hsu, Justin; Sato, Tetsuya; Strub, Pierre-Yves 2 2017 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 On the equality of probabilistic terms. Zbl 1311.94068 Barthe, Gilles; Daubignard, Marion; Kapron, Bruce; Lakhnech, Yassine; Laporte, Vincent 2 2010 Programming language techniques for cryptographic proofs. Zbl 1291.68323 Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago 2 2010 Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14–18, 2011. Proceedings. Zbl 1225.68009 2 2011 Security types preserving compilation. (Extended abstract). Zbl 1202.68085 Barthe, Gilles; Basu, Amitabh; Rezk, Tamara 2 2004 Probabilistic relational Hoare logics for computer-aided security proofs. Zbl 1358.94059 Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago 2 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 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 Expanding the cube. Zbl 0932.03013 Barthe, Gilles 1 1999 Monadic type systems: Pure type systems for impure settings. (Preliminary report). Zbl 0925.68294 Barthe, Gilles; Hatcliff, John; Thiemann, Peter 1 1997 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 A formal treatment of the role of verified compilers in secure computation. Zbl 1542.68030 Bacelar Almeida, José Carlos; Barbosa, Manuel; Barthe, Gilles; Pacheco, Hugo; Pereira, Vitor; Portela, Bernardo 1 2022 Preservation of proof obligations from Java to the Java virtual machine. Zbl 1165.68398 Barthe, Gilles; Grégoire, Benjamin; Pavlova, Mariela 1 2008 Automated analysis of cryptographic assumptions in generic group models. Zbl 1434.94057 Barthe, Gilles; Fagerholm, Edvard; Fiore, Dario; Mitchell, John; Scedrov, Andre; Schmidt, Benedikt 1 2019 Relational reasoning for Markov chains in a probabilistic guarded lambda calculus. Zbl 1418.68048 Aguirre, Alejandro; Barthe, Gilles; Birkedal, Lars; Bizjak, Aleš; Gaboardi, Marco; Garg, Deepak 1 2018 Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. Zbl 1468.68057 Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo 1 2019 Foundations of security analysis and design V. FOSAD 2007/2008/2009 tutorial lectures. Zbl 1173.68001 1 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 Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9–15, 2000. Advanced lectures. Zbl 0993.00046 1 2002 A simple abstract semantics for equational theories. Zbl 1507.68201 Barthe, Gilles 1 1995 A formal treatment of the role of verified compilers in secure computation. Zbl 1542.68030 Bacelar Almeida, José Carlos; Barbosa, Manuel; Barthe, Gilles; Pacheco, Hugo; Pereira, Vitor; Portela, Bernardo 1 2022 Foundations of probabilistic programming. Zbl 1458.68003 4 2021 On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem. Zbl 1508.68055 Barthe, Gilles; Crubillé, Raphaëlle; Dal Lago, Ugo; Gavazzo, Francesco 9 2020 Deciding differential privacy for programs with finite inputs and outputs. Zbl 1507.68111 Barthe, Gilles; Chadha, Rohit; Jagannath, Vishal; Sistla, A. Prasad; Viswanathan, Mahesh 6 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 5 2020 Universal equivalence and majority of probabilistic programs over finite fields. Zbl 1496.68186 Barthe, Gilles; Jacomme, Charlie; Kremer, Steve 3 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 Automated analysis of cryptographic assumptions in generic group models. Zbl 1434.94057 Barthe, Gilles; Fagerholm, Edvard; Fiore, Dario; Mitchell, John; Scedrov, Andre; Schmidt, Benedikt 1 2019 Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. Zbl 1468.68057 Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo 1 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 18 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 3 2018 Relational reasoning for Markov chains in a probabilistic guarded lambda calculus. Zbl 1418.68048 Aguirre, Alejandro; Barthe, Gilles; Birkedal, Lars; Bizjak, Aleš; Gaboardi, Marco; Garg, Deepak 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 24 2017 Generic transformations of predicate encodings: constructions and applications. Zbl 1407.94069 Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt 18 2017 Relational cost analysis. Zbl 1380.68118 Çiçek, Ezgi; Barthe, Gilles; Gaboardi, Marco; Garg, Deepak; Hoffmann, Jan 5 2017 Coupling proofs are probabilistic product programs. Zbl 1380.68267 Barthe, Gilles; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves 4 2017 Is your software on dope? Formal analysis of surreptitiously “enhanced” programs. Zbl 1485.68059 D’Argenio, Pedro R.; Barthe, Gilles; Biewer, Sebastian; Finkbeiner, Bernd; Hermanns, Holger 3 2017 \(*\)-liftings for differential privacy. Zbl 1442.68100 Barthe, Gilles; Espitau, Thomas; Hsu, Justin; Sato, Tetsuya; Strub, Pierre-Yves 2 2017 Proving differential privacy via probabilistic couplings. Zbl 1401.68184 Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves 17 2016 Synthesizing probabilistic invariants via Doob’s decomposition. Zbl 1411.68057 Barthe, Gilles; Espitau, Thomas; Ferrer Fioriti, Luis María; Hsu, Justin 15 2016 Automated unbounded analysis of cryptographic constructions in the generic group model. Zbl 1371.94618 Ambrona, Miguel; Barthe, Gilles; Schmidt, Benedikt 6 2016 Product programs and relational program logics. Zbl 1355.68047 Barthe, Gilles; Crespo, Juan Manuel; Kunz, César 6 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 3 2016 A program logic for union bounds. Zbl 1388.68022 Barthe, Gilles; Gaboardi, Marco; Grégoire, Benjamin; Hsu, Justin; Strub, Pierre-Yves 3 2016 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 27 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 15 2015 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 11 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 4 2015 Implicit computational complexity of subrecursive definitions and applications to cryptographic proofs. Zbl 1471.68053 Baillot, Patrick; Barthe, Gilles; Dal Lago, Ugo 4 2015 Relational reasoning via probabilistic coupling. Zbl 1471.68127 Barthe, Gilles; Espitau, Thomas; Grégoire, Benjamin; Hsu, Justin; Stefanesco, Léo; Strub, Pierre-Yves 3 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 18 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 11 2014 EasyCrypt: a tutorial. Zbl 1448.68184 Barthe, Gilles; Dupressoir, François; Grégoire, Benjamin; Kunz, César; Schmidt, Benedikt; Strub, Pierre-Yves 9 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 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 11 2013 Beyond differential privacy: composition theorems and relational logic for \(f\)-divergences between probabilistic programs. Zbl 1335.68043 Barthe, Gilles; Olmedo, Federico 8 2013 Probabilistic relational reasoning for differential privacy. Zbl 1321.68182 Barthe, Gilles; Köpf, Boris; Olmedo, Federico; Zanella Béguelin, Santiago 31 2012 Computer-aided cryptographic proofs. Zbl 1360.94294 Barthe, Gilles; Crespo, Juan Manuel; Grégoire, Benjamin; Kunz, César; Zanella Béguelin, Santiago 5 2012 Probabilistic relational Hoare logics for computer-aided security proofs. Zbl 1358.94059 Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago 2 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 Secure information flow by self-composition. Zbl 1252.68072 Barthe, Gilles; D’Argenio, Pedro R.; Rezk, Tamara 32 2011 Computer-aided security proofs for the working cryptographer. Zbl 1287.94048 Barthe, Gilles; Grégoire, Benjamin; Heraud, Sylvain; Béguelin, Santiago Zanella 25 2011 Beyond provable security verifiable IND-CCA security of OAEP. Zbl 1284.94052 Barthe, Gilles; Grégoire, Benjamin; Lakhnech, Yassine; Zanella Béguelin, Santiago 5 2011 Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14–18, 2011. Proceedings. Zbl 1225.68009 2 2011 On the equality of probabilistic terms. Zbl 1311.94068 Barthe, Gilles; Daubignard, Marion; Kapron, Bruce; Lakhnech, Yassine; Laporte, Vincent 2 2010 Programming language techniques for cryptographic proofs. Zbl 1291.68323 Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago 2 2010 Formal certification of code-based cryptographic proofs. Zbl 1315.68081 Barthe, Gilles; Grégoire, Benjamin; Zanella Béguelin, Santiago 49 2009 A tutorial on type-based termination. Zbl 1250.68084 Barthe, Gilles; Grégoire, Benjamin; Riba, Colin 3 2009 Foundations of security analysis and design V. FOSAD 2007/2008/2009 tutorial lectures. Zbl 1173.68001 1 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 10 2008 Formal methods for open object-based distributed systems. 10th IFIP WG 6.1 international conference, FMOODS 2008, Oslo, Norway, June 4–6, 2008. Proceedings. Zbl 1137.68301 7 2008 Certificate translation in abstract interpretation. Zbl 1133.68315 Barthe, Gilles; Kunz, César 4 2008 Preservation of proof obligations from Java to the Java virtual machine. Zbl 1165.68398 Barthe, Gilles; Grégoire, Benjamin; Pavlova, Mariela 1 2008 A certified lightweight non-interference Java bytecode verifier. Zbl 1187.68112 Barthe, Gilles; Pichardie, David; Rezk, Tamara 8 2007 Security types preserving compilation. Zbl 1109.68025 Barthe, Gilles; Rezk, Tamara; Basu, Amitabh 3 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 16 2006 Certificate translation for optimizing compilers. Zbl 1225.68062 Barthe, Gilles; Grégoire, Benjamin; Kunz, César; Rezk, Tamara 10 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 6 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 7 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. 27 2004 A machine-checked formalization of the generic model and the random oracle model. Zbl 1126.68558 Barthe, Gilles; Cederquist, Jan; Tarento, Sabrina 7 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 33 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 4 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 An introduction to dependent type theory. Zbl 1065.68025 Barthe, Gilles; Coquand, Thierry 3 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 Type isomorphisms and proof reuse in dependent type theory. Zbl 0978.68044 Barthe, Gilles; Pons, Olivier 9 2001 A formal executable semantics of the JavaCard platform. Zbl 0977.68577 Barthe, Gilles; Dufay, Guillaume; Jakubiec, Line; Serpette, Bernard; de Sousa, Simão Melo 7 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 3 2001 Domain-free pure type systems. Zbl 0979.03013 Barthe, Gilles; Sørensen, Morten Heine 13 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. 10 1999 Type-checking injective pure type systems. Zbl 0949.03027 Barthe, Gilles 4 1999 Existence and uniqueness of normal forms in pure type systems with \(\beta\eta\)-conversion. Zbl 0933.03008 Barthe, Gilles 3 1999 Partial evaluation and non-interference for object calculi. Zbl 0988.68049 Barthe, Gilles; Serpette, Bernard P. 2 1999 Expanding the cube. Zbl 0932.03013 Barthe, Gilles 1 1999 Order-sorted inductive types. Zbl 0928.68022 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 notion of classical pure type system. Zbl 0911.68109 Barthe, Gilles; Hatcliff, John; Sørenson, Morten 2 1997 Monadic type systems: Pure type systems for impure settings. (Preliminary report). Zbl 0925.68294 Barthe, Gilles; Hatcliff, John; Thiemann, Peter 1 1997 Implicit coercions in type systems. Zbl 1434.03081 Barthe, Gilles 5 1996 A two-level approach towards lean proof-checking. Zbl 1407.68431 Barthe, Gilles; Ruys, Mark; Barendregt, Henk 5 1996 Extensions of pure type system. Zbl 1063.03508 Barthe, Gilles 2 1995 A simple abstract semantics for equational theories. Zbl 1507.68201 Barthe, Gilles 1 1995 all cited Publications top 5 cited Publications all top 5 Cited by 897 Authors 43 Barthe, Gilles 14 Grégoire, Benjamin 11 Strub, Pierre-Yves 10 Abel, Andreas M. 10 Katoen, Joost-Pieter 10 Standaert, Francois-Xavier 9 Gaboardi, Marco 9 Hsu, Justin 8 Kirchner, Claude 8 Tibouchi, Mehdi 6 Cirstea, Horatiu 6 Dal Lago, Ugo 6 Finkbeiner, Bernd 6 Kaminski, Benjamin Lucien 6 Kunz, César 6 Pichardie, David 6 Zanella Béguelin, Santiago 5 Belaïd, Sonia 5 Blanqui, Frédéric 5 Chatterjee, Krishnendu 5 Espitau, Thomas 5 Faust, Sebastian 5 Fouque, Pierre-Alain 5 Fujita, Ken-etsu 5 Lakhnech, Yassine 5 Lochbihler, Andreas 5 Maietti, Maria Emilia 5 Matheja, Christoph 5 Rivain, Matthieu 5 Sørensen, Morten Heine B. 4 Barbosa, Manuel 4 Batz, Kevin 4 Dupressoir, François 4 Ene, Cristian 4 Kohlweiss, Markulf 4 Liquori, Luigi 4 Novotný, Petr 4 Nowak, David E. 4 Olmedo, Federico 4 Primas, Robert 4 Sato, Tetsuya 4 Stratulat, Sorin 4 Takahashi, Akira 4 Tassi, Enrico 4 Vákár, Matthijs 4 Žikelić, {D}or{d}e 3 Abe, Masayuki 3 Affeldt, Reynald 3 Allamigeon, Xavier 3 Bacelar Almeida, José 3 Baillot, Patrick 3 Bartocci, Ezio 3 Beringer, Lennart 3 Bertolissi, Clara 3 Bertot, Yves 3 Beutner, Raven 3 Bloem, Roderick 3 Cassiers, Gaëtan 3 Chen, Mingshuai 3 Coron, Jean-Sébastien 3 Crespo, Juan Manuel 3 Fantechi, Alessandro 3 Faure, Germain 3 Fiore, Dario 3 Fournet, Cédric 3 Gascón, Adrià 3 Geuvers, Jan Herman 3 Ghadafi, Essam M. 3 Gong, Junqing 3 Guilley, Sylvain 3 Güneysu, Tim 3 Gurov, Dilian 3 Hatcliff, John 3 Hoffmann, Jan-Philipp 3 Hofmann, Martin 3 Jacobs, Bart 3 Katsumata, Shin-ya 3 Kovács, Laura Ildikó 3 Krauss, Alexander 3 Lafourcade, Pascal 3 Leroy, Xavier 3 Mangard, Stefan 3 Melo de Sousa, Simão 3 Momin, Charles 3 Nakazawa, Koji 3 Nipkow, Tobias 3 Orlandi, Claudio 3 Petit, Barbara 3 Pinto, Jorge Sousa 3 Prest, Thomas 3 Rezk, Tamara 3 Riba, Colin 3 Rosolini, Giuseppe 3 Rossi, Mélissa 3 Schubert, Aleksy 3 Setzer, Anton 3 Slamanig, Daniel 3 Staton, Sam 3 Stump, Aaron 3 Swamy, Nikhil ...and 797 more Authors all top 5 Cited in 43 Serials 29 Theoretical Computer Science 21 Journal of Automated Reasoning 13 Information and Computation 13 Journal of Functional Programming 12 The Journal of Logic and Algebraic Programming 11 Logical Methods in Computer Science 11 Journal of Logical and Algebraic Methods in Programming 9 Journal of Cryptology 8 Mathematical Structures in Computer Science 5 Science of Computer Programming 4 Annals of Pure and Applied Logic 4 Formal Aspects of Computing 4 Designs, Codes and Cryptography 4 Formal Methods in System Design 3 Journal of Symbolic Computation 3 Computer Languages, Systems & Structures 2 Acta Informatica 2 Discrete Event Dynamic Systems 2 Archive for Mathematical Logic 2 Annals of Mathematics and Artificial Intelligence 2 Higher-Order and Symbolic Computation 2 RAIRO. Theoretical Informatics and Applications 2 ACM Transactions on Computational Logic 2 Journal of Applied Logic 2 Cryptography and Communications 2 Journal of Formalized Reasoning 1 Communications in Mathematical Physics 1 Mathematical Methods in the Applied Sciences 1 Journal of Pure and Applied Algebra 1 The Journal of Symbolic Logic 1 SIAM Journal on Computing 1 Studia Logica 1 Journal of Complexity 1 Journal of Computer Science and Technology 1 Indagationes Mathematicae. New Series 1 Applied Categorical Structures 1 Journal of Inequalities and Applications 1 Journal of the ACM 1 Theory and Practice of Logic Programming 1 Sādhanā 1 Logica Universalis 1 Tbilisi Mathematical Journal 1 Computer Science Review all top 5 Cited in 27 Fields 365 Computer science (68-XX) 150 Information and communication theory, circuits (94-XX) 122 Mathematical logic and foundations (03-XX) 16 Category theory; homological algebra (18-XX) 14 Quantum theory (81-XX) 8 Operations research, mathematical programming (90-XX) 4 Number theory (11-XX) 4 Algebraic topology (55-XX) 4 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 3 Order, lattices, ordered algebraic structures (06-XX) 3 Probability theory and stochastic processes (60-XX) 3 Statistics (62-XX) 2 General and overarching topics; collections (00-XX) 2 Group theory and generalizations (20-XX) 2 Convex and discrete geometry (52-XX) 2 Numerical analysis (65-XX) 2 Biology and other natural sciences (92-XX) 2 Systems theory; control (93-XX) 1 History and biography (01-XX) 1 Combinatorics (05-XX) 1 General algebraic systems (08-XX) 1 Field theory and polynomials (12-XX) 1 Commutative algebra (13-XX) 1 Algebraic geometry (14-XX) 1 Linear and multilinear algebra; matrix theory (15-XX) 1 Partial differential equations (35-XX) 1 Geometry (51-XX) Citations by Year