default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDGilles Barthe
Person information
- affiliation: Max Planck Institute for Security and Privacy, Bochum, Germany
- affiliation (2008 - 2018): IMDEA Software Institute, Spain
- affiliation (1999 - 2008): INRIA, Sophia-Antipolis, France
- affiliation (1998 - 1999): University of Minho, Braga, Portugal
- affiliation (1997 - 1998): Chalmers University, Gothenburg, Sweden
- affiliation (1995 - 1997): Centrum Wiskunde & Informatica, Amsterdam, The Netherlands
- affiliation (1993 - 1995): University of Nijmegen, The Netherlands
- affiliation (PhD 1993): University of Manchester, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j62]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. J. Cryptol. 37(1): 5 (2024)- [j61]Martin Avanzini, Gilles Barthe
, Benjamin Grégoire, Georg Moser, Gabriele Vanoni:
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. Proc. ACM Program. Lang. 8(OOPSLA1): 784-809 (2024) - [j60]Vineet Rajani, Gilles Barthe, Deepak Garg:
A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs. Proc. ACM Program. Lang. 8(OOPSLA2): 389-414 (2024) - [j59]Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind:
Decision and Complexity of Dolev-Yao Hyperproperties. Proc. ACM Program. Lang. 8(POPL): 1913-1944 (2024) - [j58]Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe:
High-assurance zeroization. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2024(1): 375-397 (2024) - [c195]Elizaveta Vasilenko, Niki Vazou, Gilles Barthe:
OBRA: Oracle-Based, Relational, Algorithmic Type Verification. APLAS 2024: 283-302 - [c194]Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom:
Testing Side-channel Security of Cryptographic Implementations against Future Microarchitectures. CCS 2024: 1076-1090 - [c193]José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub:
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) 2024: 384-421 - [c192]Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar:
They're not that hard to mitigate: What Cryptographic Library Developers Think About Timing Attacks. Software Engineering 2024: 143-144 - [c191]Marcel Fourné, Daniel De Almeida Braga, Jan Jancar, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar:
"These results must be false": A usability evaluation of constant-time analysis tools. USENIX Security Symposium 2024 - [i99]Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom:
Testing side-channel security of cryptographic implementations against future microarchitectures. CoRR abs/2402.00641 (2024) - [i98]Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire:
A quantitative probabilistic relational Hoare logic. CoRR abs/2407.17127 (2024) - [i97]José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub:
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. IACR Cryptol. ePrint Arch. 2024: 843 (2024) - [i96]Santiago Arranz Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang:
Protecting cryptographic code against Spectre-RSB. IACR Cryptol. ePrint Arch. 2024: 1070 (2024) - [i95]Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte:
Preservation of Speculative Constant-time by Compilation. IACR Cryptol. ePrint Arch. 2024: 1203 (2024) - 2023
- [j57]Amir-Hossein Karimi, Gilles Barthe, Bernhard Schölkopf, Isabel Valera:
A Survey of Algorithmic Recourse: Contrastive Explanations and Consequential Recommendations. ACM Comput. Surv. 55(5): 95:1-95:29 (2023) - [j56]Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying:
CoqQ: Foundational Verification of Quantum Programs. Proc. ACM Program. Lang. 7(POPL): 833-865 (2023) - [j55]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub:
Formally verifying Kyber Episode IV: Implementation correctness. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2023(3): 164-193 (2023) - [j54]Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub:
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. ACM Trans. Priv. Secur. 26(3): 41:1-41:34 (2023) - [c190]Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu:
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. CRYPTO (5) 2023: 358-389 - [c189]Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean:
Typing High-Speed Cryptography against Spectre v1. SP 2023: 1094-1111 - [c188]Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O'Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom:
Spectre Declassified: Reading from the Right Place at the Wrong Time. SP 2023: 1753-1770 - [c187]Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom:
Ultimate SLH: Taking Speculative Load Hardening to the Next Level. USENIX Security Symposium 2023: 7125-7142 - [i94]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub:
Formally verifying Kyber Part I: Implementation Correctness. IACR Cryptol. ePrint Arch. 2023: 215 (2023) - [i93]Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu:
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. IACR Cryptol. ePrint Arch. 2023: 246 (2023) - [i92]Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe:
High-assurance zeroization. IACR Cryptol. ePrint Arch. 2023: 1713 (2023) - 2022
- [j53]José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela:
A formal treatment of the role of verified compilers in secure computation. J. Log. Algebraic Methods Program. 125: 100736 (2022) - [j52]Elizaveta Vasilenko, Niki Vazou, Gilles Barthe:
Safe couplings: coupled refinement types. Proc. ACM Program. Lang. 6(ICFP): 596-624 (2022) - [j51]Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo:
On Feller continuity and full abstraction. Proc. ACM Program. Lang. 6(ICFP): 826-854 (2022) - [j50]Gilles Barthe, Charlie Jacomme, Steve Kremer:
Universal Equivalence and Majority of Probabilistic Programs over Finite Fields. ACM Trans. Comput. Log. 23(1): 5:1-5:42 (2022) - [c186]Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe:
Symbolic Synthesis of Indifferentiability Attacks. AsiaCCS 2022: 667-681 - [c185]Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Enforcing Fine-grained Constant-time Policies. CCS 2022: 83-96 - [c184]Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, Itsaka Rakotonirina:
Tidy: Symbolic Verification of Timed Cryptographic Protocols. CCS 2022: 263-276 - [c183]Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying:
Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. LICS 2022: 4:1-4:13 - [c182]Gilles Barthe, Adrien Koutsos, Solène Mirliaz, David Pichardie, Peter Schwabe:
Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs. SAS 2022: 372-396 - [c181]Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar:
"They're not that hard to mitigate": What Cryptographic Library Developers Think About Timing Attacks. SP 2022: 632-649 - [c180]Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan:
SoK: Practical Foundations for Software Spectre Defenses. SP 2022: 666-680 - [i91]Nico Lehmann, Adam T. Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala:
Flux: Liquid Types for Rust. CoRR abs/2207.04034 (2022) - [i90]Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo:
On Feller Continuity and Full Abstraction (Long Version). CoRR abs/2207.10590 (2022) - [i89]Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying:
CoqQ: Foundational Verification of Quantum Programs. CoRR abs/2207.11350 (2022) - [i88]Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O'Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom:
Spectre Declassified: Reading from the Right Place at the Wrong Time. IACR Cryptol. ePrint Arch. 2022: 426 (2022) - [i87]Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Enforcing fine-grained constant-time policies. IACR Cryptol. ePrint Arch. 2022: 630 (2022) - [i86]Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom:
Breaking and Fixing Speculative Load Hardening. IACR Cryptol. ePrint Arch. 2022: 715 (2022) - [i85]Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean:
Typing High-Speed Cryptography against Spectre v1. IACR Cryptol. ePrint Arch. 2022: 1270 (2022) - 2021
- [j49]Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato:
Higher-order probabilistic adversarial computations: categorical semantics and program logics. Proc. ACM Program. Lang. 5(ICFP): 1-30 (2021) - [j48]Martin Avanzini, Gilles Barthe, Ugo Dal Lago:
On continuation-passing transformations and expected cost analysis. Proc. ACM Program. Lang. 5(ICFP): 1-30 (2021) - [j47]Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja:
A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5(POPL): 1-28 (2021) - [j46]Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan:
Deciding accuracy of differential privacy schemes. Proc. ACM Program. Lang. 5(POPL): 1-30 (2021) - [j45]Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth:
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2021(2): 189-228 (2021) - [c179]Kiarash Mohammadi, Amir-Hossein Karimi, Gilles Barthe, Isabel Valera:
Scaling Guarantees for Nearest Counterfactual Explanations. AIES 2021: 177-187 - [c178]Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. CCS 2021: 462-476 - [c177]Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub:
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. CCS 2021: 2541-2563 - [c176]Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou:
EasyPQC: Verifying Post-Quantum Cryptography. CCS 2021: 2564-2586 - [c175]Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie:
Secure Compilation of Constant-Resource Programs. CSF 2021: 1-12 - [c174]Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu:
A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. LICS 2021: 1-14 - [c173]Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno:
SoK: Computer-Aided Cryptography. SP 2021: 777-795 - [c172]Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe:
High-Assurance Cryptography in the Spectre Era. SP 2021: 1884-1901 - [i84]Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu:
A Quantum Interpretation of Bunched Logic for Quantum Separation Logic. CoRR abs/2102.00329 (2021) - [i83]Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan:
SoK: Practical Foundations for Spectre Defenses. CoRR abs/2105.05801 (2021) - [i82]Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato:
Higher-order probabilistic adversarial computations: Categorical semantics and program logics. CoRR abs/2107.01155 (2021) - [i81]Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub:
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. IACR Cryptol. ePrint Arch. 2021: 156 (2021) - [i80]Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. IACR Cryptol. ePrint Arch. 2021: 650 (2021) - [i79]Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou:
EasyPQC: Verifying Post-Quantum Cryptography. IACR Cryptol. ePrint Arch. 2021: 1253 (2021) - [i78]Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar:
“They’re not that hard to mitigateâ€: What Cryptographic Library Developers Think About Timing Attacks. IACR Cryptol. ePrint Arch. 2021: 1650 (2021) - 2020
- [j44]Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie:
System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory. J. Autom. Reason. 64(8): 1685-1729 (2020) - [j43]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. Cryptogr. Eng. 10(1): 17-26 (2020) - [j42]Borja Balle, Gilles Barthe, Marco Gaboardi:
Privacy Profiles and Amplification by Subsampling. J. Priv. Confidentiality 10(1) (2020) - [j41]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) - [j40]Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou:
Relational proofs for quantum programs. Proc. ACM Program. Lang. 4(POPL): 21:1-21:29 (2020) - [j39]Gilles Barthe, Justin Hsu, Kevin Liao:
A probabilistic separation logic. Proc. ACM Program. Lang. 4(POPL): 55:1-55:30 (2020) - [c171]Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera:
Model-Agnostic Counterfactual Explanations for Consequential Decisions. AISTATS 2020: 895-905 - [c170]Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, Tetsuya Sato:
Hypothesis Testing Interpretations and Renyi Differential Privacy. AISTATS 2020: 2496-2506 - [c169]Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo:
On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem. ESOP 2020: 56-83 - [c168]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira:
Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. INDOCRYPT 2020: 107-127 - [c167]Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan:
Deciding Differential Privacy for Programs with Finite Inputs and Outputs. LICS 2020: 141-154 - [c166]Gilles Barthe, Charlie Jacomme, Steve Kremer:
Universal equivalence and majority of probabilistic programs over finite fields. LICS 2020: 155-166 - [c165]Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe:
Constant-time foundations for the new spectre era. PLDI 2020: 913-926 - [c164]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. SP 2020: 965-982 - [i77]Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo:
On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem. CoRR abs/2002.08489 (2020) - [i76]Amir-Hossein Karimi, Gilles Barthe, Bernhard Schölkopf, Isabel Valera:
A survey of algorithmic recourse: definitions, formulations, solutions, and prospects. CoRR abs/2010.04050 (2020) - [i75]Kiarash Mohammadi, Amir-Hossein Karimi, Gilles Barthe, Isabel Valera:
Scaling Guarantees for Nearest Counterfactual Explanations. CoRR abs/2010.04965 (2020) - [i74]Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan:
Deciding Accuracy of Differential Privacy Schemes. CoRR abs/2011.06404 (2020) - [i73]Gilles Barthe, Roberta De Viti, Peter Druschel, Deepak Garg, Manuel Gomez-Rodriguez, Pierfrancesco Ingo, Matthew Lentz, Aastha Mehta, Bernhard Schölkopf:
PanCast: Listening to Bluetooth Beacons for Epidemic Risk Mitigation. CoRR abs/2011.08069 (2020) - [i72]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) - [i71]Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe:
High-Assurance Cryptography Software in the Spectre Era. IACR Cryptol. ePrint Arch. 2020: 1104 (2020)
2010 – 2019
- 2019
- [j38]Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna:
System-Level Non-interference of Constant-Time Cryptography. Part I: Model. J. Autom. Reason. 63(1): 1-51 (2019) - [j37]Patrick Baillot, Gilles Barthe, Ugo Dal Lago:
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. J. Autom. Reason. 63(4): 813-855 (2019) - [j36]Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub:
A relational logic for higher-order programs. J. Funct. Program. 29: e16 (2019) - [j35]Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt:
Automated Analysis of Cryptographic Assumptions in Generic Group Models. J. Cryptol. 32(2): 324-360 (2019) - [j34]Gilles Barthe, Christos Dimitrakakis, Marco Gaboardi, Andreas Haeberlen, Aaron Roth, Aleksandra B. Slavkovic:
Program for TPDP 2016. J. Priv. Confidentiality 9(1) (2019) - [j33]Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub:
Relational ⋆⋆\star-Liftings for Differential Privacy. Log. Methods Comput. Sci. 15(4) (2019) - [j32]Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu:
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization. Proc. ACM Program. Lang. 3(POPL): 38:1-38:30 (2019) - [c163]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. CCS 2019: 63-78 - [c162]José Bacelar Almeida, Cécile 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. CCS 2019: 1607-1622 - [c161]Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Mélissa Rossi, Mehdi Tibouchi:
GALACTICS: Gaussian Sampling for Lattice-Based Constant- Time Implementation of Cryptographic Signatures, Revisited. CCS 2019: 2147-2164 - [c160]Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub:
Symbolic Methods in Computational Cryptography Proofs. CSF 2019: 136-151 - [c159]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 - [c158]Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei:
Verifying Relational Properties using Trace Logic. FMCAD 2019: 170-178 - [c157]Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata:
Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. LICS 2019: 1-14 - [c156]Borja Balle, Gilles Barthe, Marco Gaboardi, Joseph Geumlek:
Privacy Amplification by Mixing and Diffusion Mechanisms. NeurIPS 2019: 13277-13287 - [c155]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 - [c154]Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg:
Bidirectional type checking for relational properties. PLDI 2019: 533-547 - [i70]Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou:
Coupling Techniques for Reasoning about Quantum Programs. CoRR abs/1901.05184 (2019) - [i69]Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja:
Kantorovich Continuity of Probabilistic Programs. CoRR abs/1901.06540 (2019) - [i68]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) - [i67]Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, Tetsuya Sato:
Hypothesis Testing Interpretations and Renyi Differential Privacy. CoRR abs/1905.09982 (2019) - [i66]Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera:
Model-Agnostic Counterfactual Explanations for Consequential Decisions. CoRR abs/1905.11190 (2019) - [i65]Borja Balle, Gilles Barthe, Marco Gaboardi, Joseph Geumlek:
Privacy Amplification by Mixing and Diffusion Mechanisms. CoRR abs/1905.12264 (2019) - [i64]Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei:
Verifying Relational Properties using Trace Logic. CoRR abs/1906.09899 (2019) - [i63]Gilles Barthe, Justin Hsu, Kevin Liao:
A Probabilistic Separation Logic. CoRR abs/1907.10708 (2019) - [i62]Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Deian Stefan, Tamara Rezk, Gilles Barthe:
Towards Constant-Time Foundations for the New Spectre Era. CoRR abs/1910.01755 (2019) - [i61]Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan:
Automated Methods for Checking Differential Privacy. CoRR abs/1910.04137 (2019) - [i60]Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Mélissa Rossi, Mehdi Tibouchi:
GALACTICS: Gaussian Sampling for Lattice-Based Constant-Time Implementation of Cryptographic Signatures, Revisited. IACR Cryptol. ePrint Arch. 2019: 511 (2019) - [i59]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) - [i58]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) - [i57]José Bacelar Almeida, Cécile 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) - [i56]Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno:
SoK: Computer-Aided Cryptography. IACR Cryptol. ePrint Arch. 2019: 1393 (2019) - 2018
- [j31]Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger:
Monadic refinements for relational cost analysis. Proc. ACM Program. Lang. 2(POPL): 36:1-36:32 (2018) - [j30]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) - [c153]Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi:
Symbolic Proofs for Lattice-Based Cryptography. CCS 2018: 538-555 - [c152]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela:
Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks. CSF 2018: 132-146 - [c151]Gilles Barthe, Benjamin Grégoire, Vincent Laporte:
Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". CSF 2018: 328-343 - [c150]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 - [c149]Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg:
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. ESOP 2018: 214-241 - [c148]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 - [c147]Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva:
Almost Sure Productivity. ICALP 2018: 113:1-113:15 - [c146]Borja Balle, Gilles Barthe, Marco Gaboardi:
Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences. NeurIPS 2018: 6280-6290 - [e17]Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe, Margus Veanes:
LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018. Kalpa Publications in Computing 9, EasyChair 2018 [contents] - [e16]Gilles Barthe, Geoff Sutcliffe, Margus Veanes:
LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018. EPiC Series in Computing 57, EasyChair 2018 [contents] - [i55]Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva:
Almost Sure Productivity. CoRR abs/1802.06283 (2018) - [i54]Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg:
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. CoRR abs/1802.09787 (2018) - [i53]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) - [i52]Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, Holger Hermanns:
Facets of Software Doping. CoRR abs/1803.10154 (2018) - [i51]Borja Balle, Gilles Barthe, Marco Gaboardi:
Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences. CoRR abs/1807.01647 (2018) - [i50]Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu:
Formal verification of higher-order probabilistic programs. CoRR abs/1807.06091 (2018) - [i49]Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg:
Bidirectional Type Checking for Relational Properties. CoRR abs/1812.05067 (2018) - [i48]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) - [i47]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela:
Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks. IACR Cryptol. ePrint Arch. 2018: 404 (2018) - [i46]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) - [i45]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) - [i44]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
- [j29]Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub:
A relational logic for higher-order programs. Proc. ACM Program. Lang. 1(ICFP): 21:1-21:29 (2017) - [c145]Miguel Ambrona, Gilles Barthe, Romain Gay, Hoeteck Wee:
Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions. CCS 2017: 647-664 - [c144]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. CCS 2017: 1807-1823 - [c143]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. CCS 2017: 1989-2006 - [c142]Miguel Ambrona, Gilles Barthe, Benedikt Schmidt:
Generic Transformations of Predicate Encodings: Constructions and Applications. CRYPTO (1) 2017: 36-66 - [c141]Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu:
Verified Translation Validation of Static Analyses. CSF 2017: 405-419 - [c140]Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns:
Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs. ESOP 2017: 83-110 - [c139]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 - [c138]Martín Ochoa, Sebastian Banescu, Cynthia Disenfeld, Gilles Barthe, Vijay Ganesh:
Reasoning about Probabilistic Defense Mechanisms against Remote Attacks. EuroS&P 2017: 499-513 - [c137]Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub:
*-Liftings for Differential Privacy. ICALP 2017: 102:1-102:12 - [c136]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 - [c135]Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. POPL 2017: 161-174 - [c134]Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann:
Relational cost analysis. POPL 2017: 316-329 - [i43]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) - [i42]Martín Ochoa, Sebastian Banescu, Cynthia Disenfeld, Gilles Barthe, Vijay Ganesh:
Reasoning about Probabilistic Defense Mechanisms against Remote Attacks. CoRR abs/1701.06743 (2017) - [i41]Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns:
Is your software on dope? Formal analysis of surreptitiously "enhanced" programs. CoRR abs/1702.04693 (2017) - [i40]Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub:
A Relational Logic for Higher-Order Programs. CoRR abs/1703.05042 (2017) - [i39]Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub:
*-Liftings for Differential Privacy. CoRR abs/1705.00133 (2017) - [i38]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Expected Sensitivity of Probabilistic Programs. CoRR abs/1708.02537 (2017) - [i37]Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata:
Reasoning about Divergences for Relaxations of Differential Privacy. CoRR abs/1710.09010 (2017) - [i36]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) - [i35]Miguel Ambrona, Gilles Barthe, Romain Gay, Hoeteck Wee:
Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions. IACR Cryptol. ePrint Arch. 2017: 983 (2017) - [i34]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) - [i33]Gilles Barthe, Benjamin Grégoire, Vincent Laporte:
Provably secure compilation of side-channel countermeasures. IACR Cryptol. ePrint Arch. 2017: 1233 (2017) - 2016
- [j28]Gilles Barthe, Edvard Fagerholm, Dario Fiore, Andre Scedrov, Benedikt Schmidt, Mehdi Tibouchi:
Strongly-optimal structure preserving signatures from Type II pairings: synthesis and lower bounds. IET Inf. Secur. 10(6): 358-371 (2016) - [j27]Gilles Barthe, Juan Manuel Crespo, César Kunz:
Product programs and relational program logics. J. Log. Algebraic Methods Program. 85(5): 847-859 (2016) - [j26]Gilles Barthe, Marco Gaboardi, Justin Hsu, Benjamin C. Pierce:
Programming language techniques for differential privacy. ACM SIGLOG News 3(1): 34-53 (2016) - [c133]Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu:
Synthesizing Probabilistic Invariants via Doob's Decomposition. CAV (1) 2016: 43-61 - [c132]Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. CCS 2016: 55-67 - [c131]Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub:
Differentially Private Bayesian Programming. CCS 2016: 68-79 - [c130]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. CCS 2016: 116-129 - [c129]Miguel Ambrona, Gilles Barthe, Benedikt Schmidt:
Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model. EUROCRYPT (2) 2016: 822-851 - [c128]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir:
Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. FSE 2016: 163-184 - [c127]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A Program Logic for Union Bounds. ICALP 2016: 107:1-107:15 - [c126]Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, Holger Hermanns:
Facets of Software Doping. ISoLA (2) 2016: 601-608 - [c125]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. LICS 2016: 749-758 - [c124]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi:
Verifying Constant-Time Implementations. USENIX Security Symposium 2016: 53-70 - [c123]Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub:
Computer-Aided Verification for Mechanism Design. WINE 2016: 279-293 - [e15]Gilles Barthe, Evangelos P. Markatos, Pierangela Samarati:
Security and Trust Management - 12th International Workshop, STM 2016, Heraklion, Crete, Greece, September 26-27, 2016, Proceedings. Lecture Notes in Computer Science 9871, Springer 2016, ISBN 978-3-319-46597-5 [contents] - [i32]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. CoRR abs/1601.05047 (2016) - [i31]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A program logic for union bounds. CoRR abs/1602.05681 (2016) - [i30]Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub:
Differentially Private Bayesian Programming. CoRR abs/1605.00283 (2016) - [i29]Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu:
Synthesizing Probabilistic Invariants via Doob's Decomposition. CoRR abs/1605.02765 (2016) - [i28]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. CoRR abs/1606.07143 (2016) - [i27]Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. CoRR abs/1607.03455 (2016) - [i26]Miguel Ambrona, Gilles Barthe, Benedikt Schmidt:
Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model. IACR Cryptol. ePrint Arch. 2016: 270 (2016) - [i25]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) - [i24]Miguel Ambrona, Gilles Barthe, Benedikt Schmidt:
Generic Transformations of Predicate Encodings: Constructions and Applications. IACR Cryptol. ePrint Arch. 2016: 1105 (2016) - 2015
- [j25]Gilles Barthe:
High-Assurance Cryptography: Cryptographic Software We Can Trust. IEEE Secur. Priv. 13(5): 86-89 (2015) - [j24]Gilles Barthe, Alberto Pardo, Gerardo Schneider:
SEFM: software engineering and formal methods. Softw. Syst. Model. 14(1): 3-4 (2015) - [c122]Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt:
Automated Proofs of Pairing-Based Cryptography. CCS 2015: 1156-1168 - [c121]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 - [c120]Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt:
Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols. EUROCRYPT (2) 2015: 689-718 - [c119]Patrick Baillot, Gilles Barthe, Ugo Dal Lago:
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. LPAR 2015: 203-218 - [c118]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub:
Relational Reasoning via Probabilistic Coupling. LPAR 2015: 387-401 - [c117]Gilles Barthe, Edvard Fagerholm, Dario Fiore, Andre Scedrov, Benedikt Schmidt, Mehdi Tibouchi:
Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds. Public Key Cryptography 2015: 355-376 - [c116]Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub:
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. POPL 2015: 55-68 - [i23]Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub:
Computer-aided verification in mechanism design. CoRR abs/1502.04052 (2015) - [i22]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) - [i21]Gilles Barthe, Andrew D. Gordon, Joost-Pieter Katoen, Annabelle McIver:
Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181). Dagstuhl Reports 5(4): 123-141 (2015) - [i20]Gilles Barthe, Edvard Fagerholm, Dario Fiore, Andre Scedrov, Benedikt Schmidt, Mehdi Tibouchi:
Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds. IACR Cryptol. ePrint Arch. 2015: 19 (2015) - [i19]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) - [i18]Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt:
Mind the Gap: Modular Machine-checked Proofs of One-Round Key Exchange Protocols. IACR Cryptol. ePrint Arch. 2015: 74 (2015) - [i17]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) - [i16]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir:
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. IACR Cryptol. ePrint Arch. 2015: 1241 (2015) - 2014
- [j23]Gilles Barthe, Delphine Demange, David Pichardie:
Formal Verification of an SSA-Based Middle-End for CompCert. ACM Trans. Program. Lang. Syst. 36(1): 4:1-4:35 (2014) - [c115]Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz:
Synthesis of Fault Attacks on Cryptographic Implementations. CCS 2014: 1016-1027 - [c114]Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, David Pichardie:
System-level Non-interference for Constant-time Cryptography. CCS 2014: 1267-1279 - [c113]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 - [c112]Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt:
Automated Analysis of Cryptographic Assumptions in Generic Group Models. CRYPTO (1) 2014: 95-112 - [c111]Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub:
Certified Synthesis of Efficient Batch Verifiers. CSF 2014: 153-165 - [c110]Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub:
Proving Differential Privacy in Hoare Logic. CSF 2014: 411-424 - [c109]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 - [c108]Gilles Barthe, Boris Köpf, Laurent Mauborgne, Martín Ochoa:
Leakage Resilience against Concurrent Cache Attacks. POST 2014: 140-158 - [i15]Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub:
Proving differential privacy in Hoare logic. CoRR abs/1407.2988 (2014) - [i14]Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub:
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. CoRR abs/1407.6845 (2014) - [i13]Gilles Barthe, Michael Hicks, Florian Kerschbaum, Dominique Unruh:
The Synergy Between Programming Languages and Cryptography (Dagstuhl Seminar 14492). Dagstuhl Reports 4(12): 29-47 (2014) - [i12]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) - [i11]Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie:
System-level non-interference for constant-time cryptography. IACR Cryptol. ePrint Arch. 2014: 422 (2014) - [i10]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) - [i9]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) - [i8]Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt:
Automated Analysis of Cryptographic Assumptions in Generic Group Models. IACR Cryptol. ePrint Arch. 2014: 458 (2014) - 2013
- [j22]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) - [j21]Gilles Barthe, David Pichardie, Tamara Rezk:
A certified lightweight non-interference Java bytecode verifier. Math. Struct. Comput. Sci. 23(5): 1032-1081 (2013) - [j20]Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin:
Probabilistic Relational Reasoning for Differential Privacy. ACM Trans. Program. Lang. Syst. 35(3): 9:1-9:49 (2013) - [c107]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir:
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. CCS 2013: 1217-1230 - [c106]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. CCS 2013: 1247-1260 - [c105]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 - [c104]Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub:
EasyCrypt: A Tutorial. FOSAD 2013: 146-166 - [c103]Gilles Barthe, Federico Olmedo:
Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs. ICALP (2) 2013: 49-60 - [c102]Gilles Barthe, Juan Manuel Crespo, César Kunz:
Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification. LFCS 2013: 29-43 - [c101]Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron:
From relational verification to SIMD loop synthesis. PPoPP 2013: 123-134 - [c100]Gilles Barthe:
Computer-Aided Security Proofs. QEST 2013: 1-2 - [c99]Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, Carlos Luna:
Formally Verified Implementation of an Idealized Model of Virtualization. TYPES 2013: 45-63 - [i7]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir:
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. IACR Cryptol. ePrint Arch. 2013: 316 (2013) - 2012
- [j19]Gilles Barthe, Jorge Cuéllar, Javier López, Alexander Pretschner:
Preface. J. Comput. Secur. 20(4): 307-308 (2012) - [c98]José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin:
Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols. CCS 2012: 488-500 - [c97]Gilles Barthe, David Pointcheval, Santiago Zanella Béguelin:
Verified security of redundancy-free encryption from Rabin and RSA. CCS 2012: 724-735 - [c96]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 - [c95]Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna:
Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization. CSF 2012: 186-197 - [c94]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 - [c93]Gilles Barthe, Delphine Demange, David Pichardie:
A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert. ESOP 2012: 47-66 - [c92]Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas:
Secure Multi-Execution through Static Program Transformation. FMOODS/FORTE 2012: 186-202 - [c91]Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin:
Computer-Aided Cryptographic Proofs. ITP 2012: 11-27 - [c90]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. MPC 2012: 1-6 - [c89]Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella Béguelin:
Probabilistic relational reasoning for differential privacy. POPL 2012: 97-110 - [c88]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin:
Verified Indifferentiable Hashing into Elliptic Curves. POST 2012: 209-228 - [c87]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Computer-Aided Cryptographic Proofs. SAS 2012: 1-2 - [e14]Gilles Barthe, Benjamin Livshits, Riccardo Scandariato:
Engineering Secure Software and Systems - 4th International Symposium, ESSoS 2012, Eindhoven, The Netherlands, February, 16-17, 2012. Proceedings. Lecture Notes in Computer Science 7159, Springer 2012, ISBN 978-3-642-28165-5 [contents] - [e13]Gilles Barthe, Anupam Datta, Sandro Etalle:
Formal Aspects of Security and Trust - 8th International Workshop, FAST 2011, Leuven, Belgium, September 12-14, 2011. Revised Selected Papers. Lecture Notes in Computer Science 7140, Springer 2012, ISBN 978-3-642-29419-8 [contents] - [i6]José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella Béguelin:
Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. IACR Cryptol. ePrint Arch. 2012: 258 (2012) - [i5]Gilles Barthe, David Pointcheval, Santiago Zanella Béguelin:
Verified Security of Redundancy-Free Encryption from Rabin and RSA. IACR Cryptol. ePrint Arch. 2012: 308 (2012) - [i4]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
- [j18]Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk:
Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6): 1207-1252 (2011) - [j17]Gilles Barthe, César Kunz:
An Abstract Model of Certificate Translation. ACM Trans. Program. Lang. Syst. 33(4): 13:1-13:46 (2011) - [c86]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin:
Computer-Aided Security Proofs for the Working Cryptographer. CRYPTO 2011: 71-90 - [c85]Gilles Barthe, Boris Köpf:
Information-Theoretic Bounds for Differentially Private Mechanisms. CSF 2011: 191-204 - [c84]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 - [c83]Gilles Barthe, Juan Manuel Crespo, César Kunz:
Relational Verification Using Product Programs. FM 2011: 200-214 - [c82]Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna:
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization. FM 2011: 231-245 - [c81]Gilles Barthe, Mathilde Duclos, Yassine Lakhnech:
A Computational Indistinguishability Logic for the Bounded Storage Model. FPS 2011: 102-117 - [c80]Gilles Barthe, Federico Olmedo, Santiago Zanella Béguelin:
Verifiable Security of Boneh-Franklin Identity-Based Encryption. ProvSec 2011: 68-83 - [c79]Gilles Barthe, Exequiel Rivas:
Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language. TGC 2011: 73-88 - [e12]Gilles Barthe:
Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings. Lecture Notes in Computer Science 6602, Springer 2011, ISBN 978-3-642-19717-8 [contents] - [e11]Gilles Barthe, Alberto Pardo, Gerardo Schneider:
Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings. Lecture Notes in Computer Science 7041, Springer 2011, ISBN 978-3-642-24689-0 [contents] - [e10]Jorge Cuéllar, Gilles Barthe, Alexander Pretschner, Javier López:
Security and Trust Management - 6th International Workshop, STM 2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers. Lecture Notes in Computer Science 6710, Springer 2011, ISBN 978-3-642-22443-0 [contents] - [i3]Gilles Barthe, Boris Köpf:
Information-theoretic Bounds for Differentially Private Mechanisms. IACR Cryptol. ePrint Arch. 2011: 71 (2011) - 2010
- [j16]Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld:
Security of multithreaded programs by compilation. ACM Trans. Inf. Syst. Secur. 13(3): 21:1-21:32 (2010) - [c78]Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech:
Computational indistinguishability logic. CCS 2010: 375-386 - [c77]Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk, Bogdan Warinschi:
Robustness Guarantees for Anonymity. CSF 2010: 91-106 - [c76]Gilles Barthe, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Grégoire, Sylvain Heraud:
A Machine-Checked Formalization of Sigma-Protocols. CSF 2010: 246-260 - [c75]Gilles Barthe, Pablo Buiras, César Kunz:
A Functional Framework for Result Checking. FLOPS 2010: 72-86 - [c74]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Programming Language Techniques for Cryptographic Proofs. ITP 2010: 115-130 - [c73]Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte:
On the Equality of Probabilistic Terms. LPAR (Dakar) 2010: 46-63 - [c72]Gilles Barthe, César Kunz:
Perspectives in Certificate Translation. TGC 2010: 23-34 - [e9]Gilles Barthe, Manuel V. Hermenegildo:
Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings. Lecture Notes in Computer Science 5944, Springer 2010, ISBN 978-3-642-11318-5 [contents]
2000 – 2009
- 2009
- [j15]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) - [c71]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet:
Implementing a Direct Method for Certificate Translation. ICFEM 2009: 541-560 - [c70]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin:
Formal certification of code-based cryptographic proofs. POPL 2009: 90-101 - [c69]Santiago Zanella Béguelin, Gilles Barthe, Benjamin Grégoire, Federico Olmedo:
Formally Certifying the Security of Digital Signature Schemes. SP 2009: 237-250 - [e8]Alessandro Aldini, Gilles Barthe, Roberto Gorrieri:
Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures. Lecture Notes in Computer Science 5705, Springer 2009, ISBN 978-3-642-03828-0 [contents] - 2008
- [c68]Gilles Barthe, César Kunz, Jorge Luis Sacchini:
Certified Reasoning in Memory Hierarchies. APLAS 2008: 75-90 - [c67]Gilles Barthe:
Certificate Translation. VERIFY 2008 - [c66]Gilles Barthe, Benjamin Grégoire, Mariela Pavlova:
Preservation of Proof Obligations from Java to the Java Virtual Machine. IJCAR 2008: 83-99 - [c65]Gilles Barthe, Salvador Cavadini, Tamara Rezk:
Tractable Enforcement of Declassification Policies. CSF 2008: 83-97 - [c64]Gilles Barthe, Benjamin Grégoire, Colin Riba:
Type-Based Termination with Sized Products. CSL 2008: 493-507 - [c63]Gilles Barthe, César Kunz:
Certificate Translation in Abstract Interpretation. ESOP 2008: 368-382 - [c62]Gilles Barthe, César Kunz:
Certificate translation for specification-preserving advices. FOAL 2008: 9-18 - [c61]Gilles Barthe, César Kunz:
An Introduction to Certificate Translation. FOSAD 2008: 51-95 - [c60]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 - [c59]Gilles Barthe, Benjamin Grégoire, Colin Riba:
A Tutorial on Type-Based Termination. LerNet ALFA Summer School 2008: 100-152 - [c58]Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese:
Preservation of Proof Pbligations for Hybrid Verification Methods. SEFM 2008: 127-136 - [e7]Gilles Barthe, Frank S. de Boer:
Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings. Lecture Notes in Computer Science 5051, Springer 2008, ISBN 978-3-540-68862-4 [contents] - [e6]Gilles Barthe, Cédric Fournet:
Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers. Lecture Notes in Computer Science 4912, Springer 2008, ISBN 978-3-540-78662-7 [contents] - 2007
- [j14]Gilles Barthe, Tamara Rezk, Amitabh Basu:
Security types preserving compilation. Comput. Lang. Syst. Struct. 33(2): 35-59 (2007) - [j13]Gilles Barthe, Leonor Prensa Nieto:
Secure information flow for a concurrent language with scheduling. J. Comput. Secur. 15(6): 647-689 (2007) - [c57]Gilles Barthe, David Pichardie, Tamara Rezk:
A Certified Lightweight Non-interference Java Bytecode Verifier. ESOP 2007: 125-140 - [c56]Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld:
Security of Multithreaded Programs by Compilation. ESORICS 2007: 2-18 - [c55]Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie:
The MOBIUS Proof Carrying Code Infrastructure. FMCO 2007: 1-24 - [e5]Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld:
Mobility, Ubiquity and Security, 25.02. - 02.03.2007. Dagstuhl Seminar Proceedings 07091, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2007 [contents] - [i2]Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld:
07091 Executive Summary - Mobility, Ubiquity and Security. Mobility, Ubiquity and Security 2007 - [i1]Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld:
07091 Abstracts Collection - Mobility, Ubiquity and Security. Mobility, Ubiquity and Security 2007 - 2006
- [j12]Gilles Barthe, Thierry Coquand:
Remarks on the equational theory of non-normalizing pure type systems. J. Funct. Program. 16(2): 137-155 (2006) - [c54]Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu:
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. FLOPS 2006: 114-129 - [c53]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 - [c52]Gilles Barthe, Benjamin Grégoire, Fernando Pastawski:
CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. LPAR 2006: 257-271 - [c51]Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk:
Certificate Translation for Optimizing Compilers. SAS 2006: 301-317 - [c50]Gilles Barthe, Tamara Rezk, David A. Naumann:
Deriving an Information Flow Checker and Certifying Compiler for Java. S&P 2006: 230-242 - [c49]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 - [e4]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
- [j11]Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa:
Tool-Assisted Specification and Verification of Typed Low-Level Languages. J. Autom. Reason. 35(4): 295-354 (2005) - [j10]Gilles Barthe:
A computational view of implicit coercions in type theory. Math. Struct. Comput. Sci. 15(5): 839-874 (2005) - [c48]Gilles Barthe, Guillaume Dufay:
Formal Methods for Smartcard Security. FOSAD 2005: 133-177 - [c47]Gilles Barthe, Tamara Rezk, Ando Saabas:
Proof Obligations Preserving Compilation. Formal Aspects in Security and Trust 2005: 112-126 - [c46]Gilles Barthe, Mariela Pavlova, Gerardo Schneider:
Precise Analysis of Memory Consumption using Program Logics. SEFM 2005: 86-95 - [c45]Gilles Barthe, Benjamin Grégoire, Fernando Pastawski:
Practical Inference for Type-Based Termination in a Polymorphic Setting. TLCA 2005: 71-85 - [c44]Gilles Barthe, Tamara Rezk:
Non-interference for a JVM-like language. TLDI 2005: 103-112 - [c43]Gilles Barthe, Tamara Rezk, Martijn Warnier:
Preventing Timing Leaks Through Transactional Branching Instructions. QAPL 2005: 33-55 - [e3]Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, Traian Muntean:
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers. Lecture Notes in Computer Science 3362, Springer 2005, ISBN 3-540-24287-2 [contents] - 2004
- [j9]Gilles Barthe, Peter Dybjer, Peter Thiemann:
Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming. J. Funct. Program. 14(1): 1-2 (2004) - [j8]Gilles Barthe, Maria João Frade, Eduardo Giménez, Luís Pinto, Tarmo Uustalu:
Type-based termination of recursive definitions. Math. Struct. Comput. Sci. 14(1): 97-141 (2004) - [c42]Gilles Barthe, Jan Cederquist, Sabrina Tarento:
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. IJCAR 2004: 385-399 - [c41]Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet:
Enforcing High-Level Security Properties for Applets. CARDIS 2004: 1-16 - [c40]Gilles Barthe, Leonor Prensa Nieto:
Formally verifying information flow type systems for concurrent and thread systems. FMSE 2004: 13-22 - [c39]Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk:
Secure Information Flow by Self-Composition. CSFW 2004: 100-114 - [c38]Gilles Barthe, Guillaume Dufay:
A Tool-Assisted Framework for Certified Bytecode Verification. FASE 2004: 99-113 - [c37]Gilles Barthe, Sabrina Tarento:
A Machine-Checked Formalization of the Random Oracle Model. TYPES 2004: 33-49 - [c36]Gilles Barthe, Amitabh Basu, Tamara Rezk:
Security Types Preserving Compilation: (Extended Abstract). VMCAI 2004: 2-15 - 2003
- [j7]Gilles Barthe, Venanzio Capretta, Olivier Pons:
Setoids in type theory. J. Funct. Program. 13(2): 261-293 (2003) - [c35]Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori:
Pure patterns type systems. POPL 2003: 250-261 - [c34]Gilles Barthe, Sorin Stratulat:
Validation of the JavaCard Platform with Implicit Induction Techniques. RTA 2003: 337-351 - [e2]Gilles Barthe, Peter Thiemann:
International Workshop in Types in Programming, TIP@MPC 2002, Dagstuhl, Germany, July 8, 2002. Electronic Notes in Theoretical Computer Science 75, Elsevier 2003 [contents] - 2002
- [c33]Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa:
Tool-Assisted Specification and Verification of the JavaCard Platform. AMAST 2002: 41-59 - [c32]Gilles Barthe, Dilian Gurov, Marieke Huisman:
Compositional Verification of Secure Applet Interactions. FASE 2002: 15-32 - [c31]Gilles Barthe, Tarmo Uustalu:
CPS translating inductive and coinductive types. PEPM 2002: 131-142 - [c30]Gilles Barthe, Pierre Courtieu:
Efficient Reasoning about Executable Specifications in Coq. TPHOLs 2002: 31-46 - [c29]Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa:
A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. VMCAI 2002: 32-45 - [c28]Gilles Barthe, Peter Thiemann:
Preface. TIP@MPC 2002: 114-115 - [e1]Gilles Barthe, Peter Dybjer, Luís Pinto, João Saraiva:
Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures. Lecture Notes in Computer Science 2395, Springer 2002, ISBN 3-540-44044-5 [contents] - 2001
- [j6]Gilles Barthe, John Hatcliff, Morten Heine Sørensen:
An induction principle for pure type systems. Theor. Comput. Sci. 266(1-2): 773-818 (2001) - [j5]Gilles Barthe, John Hatcliff, Morten Heine Sørensen:
Weak normalization implies strong normalization in a class of non-dependent pure type systems. Theor. Comput. Sci. 269(1-2): 317-361 (2001) - [c27]Gilles Barthe, Blas C. Ruiz Jiménez:
Tipos principales y cierre semi-completo para sistemas de tipos puros extendidos (trabajo en desarrollo). APPIA-GULP-PRODE 2001: 149-163 - [c26]Gilles Barthe, Guillaume Dufay, Marieke Huisman, Simão Melo de Sousa:
Jakarta: A Toolset for Reasoning about JavaCard. E-smart 2001: 2-18 - [c25]Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard P. Serpette, Simão Melo de Sousa:
A Formal Executable Semantics of the JavaCard Platform. ESOP 2001: 302-319 - [c24]Gilles Barthe, Olivier Pons:
Type Isomorphisms and Proof Reuse in Dependent Type Theory. FoSSaCS 2001: 57-71 - 2000
- [j4]Gilles Barthe, Morten Heine Sørensen:
Domain-free pure type systems. J. Funct. Program. 10(5): 417-452 (2000) - [c23]Gilles Barthe, Thierry Coquand:
An Introduction to Dependent Type Theory. APPSEM 2000: 1-41 - [c22]Gilles Barthe, Femke van Raamsdonk:
Constructor Subtyping in the Calculus of Inductive Constructions. FoSSaCS 2000: 17-34 - [c21]Gilles Barthe, Bernard P. Serpette:
Static Reduction Analysis for Imperative Object Oriented Languages. LPAR 2000: 344-361
1990 – 1999
- 1999
- [j3]Gilles Barthe:
Order-Sorted Inductive Types. Inf. Comput. 149(1): 42-76 (1999) - [j2]Gilles Barthe:
Type-checking injective pure type systems. J. Funct. Program. 9(6): 685-698 (1999) - [j1]Gilles Barthe, John Hatcliff, Morten Heine Sørensen:
CPS Translations and Applications: The Cube and Beyond. High. Order Symb. Comput. 12(2): 125-170 (1999) - [c20]Gilles Barthe, Maria João Frade:
Constructor Subtyping. ESOP 1999: 109-127 - [c19]Gilles Barthe, Bernard P. Serpette:
Partial Evaluation and Non-interference for Object Calculi. Fuji International Symposium on Functional and Logic Programming 1999: 53-67 - [c18]Gilles Barthe:
Expanding the Cube. FoSSaCS 1999: 90-103 - 1998
- [c17]Gilles Barthe:
Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion. CSL 1998: 241-259 - [c16]Gilles Barthe:
The Relevance of Proof-Irrelevance. ICALP 1998: 755-768 - [c15]Gilles Barthe:
The Semi-Full Closure of Pure Type Systems. MFCS 1998: 316-325 - 1997
- [c14]Gilles Barthe, Femke van Raamsdonk:
Termination of Algebraic Type Systems: The Syntactic Approach. ALP/HOA 1997: 174-193 - [c13]Gilles Barthe, Fairouz Kamareddine, Alejandro Ríos:
Explicit Substitutions for the Lambda-Calculus. ALP/HOA 1997: 209-223 - [c12]Gilles Barthe, Morten Heine Sørensen:
Domain-Free Pure Type Systems. LFCS 1997: 9-20 - [c11]Gilles Barthe, John Hatcliff, Morten Heine Sørensen:
Reflections on Reflections. PLILP 1997: 241-258 - [c10]Gilles Barthe, John Hatcliff, Morten Heine Sørensen:
A notion of classical pure type system. MFPS 1997: 4-59 - [c9]Gilles Barthe, John Hatcliff, Peter Thiemann:
Monadic Type Systems: Pure Type Systems for Impure Settings. HOOTS 1997: 54-120 - 1996
- [c8]Gilles Barthe, Paul-André Melliès:
On the Subject Reduction Property for Algebraic Type Systems. CSL 1996: 34-57 - [c7]Gilles Barthe, Hugo Elbers:
Towards Lean Proof Checking. DISCO 1996: 61-62 - 1995
- [c6]Gilles Barthe, Herman Geuvers:
Congruence Types. CSL 1995: 36-51 - [c5]Gilles Barthe:
A Simple Abstract Semantics for Equational Theories. FCT 1995: 126-135 - [c4]Gilles Barthe, Herman Geuvers:
Modular Properties of Algebraic Type Systems. HOA 1995: 37-56 - [c3]Gilles Barthe:
Extensions of Pure Type Systems. TLCA 1995: 16-31 - [c2]Gilles Barthe:
Implicit Coercions in Type Systems. TYPES 1995: 1-15 - [c1]Gilles Barthe, Mark Ruys, Henk Barendregt:
A Two-Level Approach Towards Lean Proof-Checking. TYPES 1995: 16-35
Coauthor Index
José Bacelar Almeida
aka: José Carlos Bacelar Almeida
aka: José Carlos Bacelar Almeida
[j62] [j61] [j58] [c193] [i98] [i97] [i96] [i95] [j55] [j54] [c190] [c189] [i94] [i93] [i92] [c185] [i87] [i85] [j45] [c178] [c177] [c176] [c172] [i81] [i80] [i79] [j43] [j41] [c164] [i72] [i71] [c163] [c162] [c160] [c159] [c155] [i68] [i59] [i58] [i57] [j30] [c153] [c151] [c150] [c148] [i53] [i48] [i46] [i45] [i44] [c144] [c143] [c139] [c136] [c135] [i43] [i38] [i36] [i34] [i33] [c132] [c130] [c127] [c125] [i32] [i31] [i28] [i27] [i25] [c122] [c121] [c118] [i22] [i19] [i17] [c115] [c113] [c111] [c109] [i12] [i10] [i9] [j22] [c106] [c105] [c104] [c96] [c94] [c91] [c90] [c88] [c87] [i4] [c86] [c84] [c76] [c74] [j15] [c71] [c70] [c69] [c66] [c64] [c60] [c59] [c55] [c53] [c52] [c51] [c49] [e4] [c45]
[c193] [i97] [j56] [j55] [j54] [i94] [i89] [c177] [c176] [i81] [i79] [j43] [c164] [j36] [j33] [c163] [c162] [c160] [i68] [i58] [i57] [j30] [c150] [i53] [i46] [j29] [c144] [c139] [c137] [c136] [c135] [i43] [i40] [i39] [i38] [c132] [c131] [c130] [c127] [c125] [c123] [i32] [i31] [i30] [i28] [i27] [i25] [c121] [c118] [c116] [i23] [i22] [i19] [c111] [c110] [c109] [i15] [i14] [i9] [c104]
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).
Privacy notice: By enabling the option above, your browser will contact the API of 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, opencitations.net, and semanticscholar.org to load article reference 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, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and 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 and semanticscholar.org 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 as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional 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 information given by OpenAlex.
last updated on 2024-12-23 20:32 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
