 | 2009 |
|---|
| 92 |       | Alessandro Aldini,
Gilles Barthe,
Roberto Gorrieri:
Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures
Springer 2009 |
| 91 | | Santiago Zanella Béguelin,
Gilles Barthe,
Benjamin Grégoire,
Federico Olmedo:
Formally Certifying the Security of Digital Signature Schemes.
IEEE Symposium on Security and Privacy 2009: 237-250 |
| 90 | | Gilles Barthe,
Benjamin Grégoire,
Santiago Zanella Béguelin:
Formal certification of code-based cryptographic proofs.
POPL 2009: 90-101 |
| 89 | | Gilles Barthe,
Benjamin Grégoire,
César Kunz,
Tamara Rezk:
Certificate translation for optimizing compilers.
ACM Trans. Program. Lang. Syst. 31(5): (2009) |
| 2008 |
|---|
| 88 |  | Gilles Barthe,
Cédric Fournet:
Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers
Springer 2008 |
| 87 | | 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
Springer 2008 |
| 86 | | Gilles Barthe,
César Kunz,
Jorge Luis Sacchini:
Certified Reasoning in Memory Hierarchies.
APLAS 2008: 75-90 |
| 85 | | Gilles Barthe,
Salvador Cavadini,
Tamara Rezk:
Tractable Enforcement of Declassification Policies.
CSF 2008: 83-97 |
| 84 | | Gilles Barthe,
Benjamin Grégoire,
Colin Riba:
Type-Based Termination with Sized Products.
CSL 2008: 493-507 |
| 83 | | Gilles Barthe,
César Kunz:
Certificate Translation in Abstract Interpretation.
ESOP 2008: 368-382 |
| 82 | | Gilles Barthe,
César Kunz:
Certificate translation for specification-preserving advices.
FOAL 2008: 9-18 |
| 81 | | Gilles Barthe,
César Kunz:
An Introduction to Certificate Translation.
FOSAD 2008: 51-95 |
| 80 | | 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 |
| 79 | | Gilles Barthe,
Benjamin Grégoire,
Mariela Pavlova:
Preservation of Proof Obligations from Java to the Java Virtual Machine.
IJCAR 2008: 83-99 |
| 78 | | Gilles Barthe,
Benjamin Grégoire,
Colin Riba:
A Tutorial on Type-Based Termination.
LerNet ALFA Summer School 2008: 100-152 |
| 77 | | Gilles Barthe,
César Kunz,
David Pichardie,
Julián Samborski-Forlese:
Preservation of Proof Pbligations for Hybrid Verification Methods.
SEFM 2008: 127-136 |
| 76 | | Gilles Barthe:
Certificate Translation.
VERIFY 2008 |
| 2007 |
|---|
| 75 | | Gilles Barthe,
Heiko Mantel,
Peter Müller,
Andrew C. Myers,
Andrei Sabelfeld:
Mobility, Ubiquity and Security, 25.02. - 02.03.2007
Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2007 |
| 74 | | Gilles Barthe,
David Pichardie,
Tamara Rezk:
A Certified Lightweight Non-interference Java Bytecode Verifier.
ESOP 2007: 125-140 |
| 73 | | Gilles Barthe,
Tamara Rezk,
Alejandro Russo,
Andrei Sabelfeld:
Security of Multithreaded Programs by Compilation.
ESORICS 2007: 2-18 |
| 72 | | Gilles Barthe,
Pierre Crégut,
Benjamin Grégoire,
Thomas P. Jensen,
David Pichardie:
The MOBIUS Proof Carrying Code Infrastructure.
FMCO 2007: 1-24 |
| 71 | | Gilles Barthe,
Heiko Mantel,
Peter Müller,
Andrew C. Myers,
Andrei Sabelfeld:
07091 Abstracts Collection - Mobility, Ubiquity and Security.
Mobility, Ubiquity and Security 2007 |
| 70 | | Gilles Barthe,
Heiko Mantel,
Peter Müller,
Andrew C. Myers,
Andrei Sabelfeld:
07091 Executive Summary - Mobility, Ubiquity and Security.
Mobility, Ubiquity and Security 2007 |
| 69 | | Gilles Barthe,
Leonor Prensa Nieto:
Secure information flow for a concurrent language with scheduling.
Journal of Computer Security 15(6): 647-689 (2007) |
| 2006 |
|---|
| 68 | | 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
Springer 2006 |
| 67 | | 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 |
| 66 | | 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 |
| 65 | | Gilles Barthe,
Tamara Rezk,
David A. Naumann:
Deriving an Information Flow Checker and Certifying Compiler for Java.
IEEE Symposium on Security and Privacy 2006: 230-242 |
| 64 | | Gilles Barthe,
Benjamin Grégoire,
Fernando Pastawski:
CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions.
LPAR 2006: 257-271 |
| 63 | | Gilles Barthe,
Benjamin Grégoire,
César Kunz,
Tamara Rezk:
Certificate Translation for Optimizing Compilers.
SAS 2006: 301-317 |
| 62 | | 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 |
| 61 | | Gilles Barthe,
Tamara Rezk,
Martijn Warnier:
Preventing Timing Leaks Through Transactional Branching Instructions.
Electr. Notes Theor. Comput. Sci. 153(2): 33-55 (2006) |
| 60 | | Gilles Barthe,
Thierry Coquand:
Remarks on the equational theory of non-normalizing pure type systems.
J. Funct. Program. 16(2): 137-155 (2006) |
| 2005 |
|---|
| 59 | | 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
Springer 2005 |
| 58 | | Gilles Barthe,
Guillaume Dufay:
Formal Methods for Smartcard Security.
FOSAD 2005: 133-177 |
| 57 | | Gilles Barthe,
Tamara Rezk,
Ando Saabas:
Proof Obligations Preserving Compilation.
Formal Aspects in Security and Trust 2005: 112-126 |
| 56 | | Gilles Barthe,
Mariela Pavlova,
Gerardo Schneider:
Precise Analysis of Memory Consumption using Program Logics.
SEFM 2005: 86-95 |
| 55 | | Gilles Barthe,
Benjamin Grégoire,
Fernando Pastawski:
Practical Inference for Type-Based Termination in a Polymorphic Setting.
TLCA 2005: 71-85 |
| 54 | | Gilles Barthe,
Tamara Rezk:
Non-interference for a JVM-like language.
TLDI 2005: 103-112 |
| 53 | | Gilles Barthe,
Pierre Courtieu,
Guillaume Dufay,
Simão Melo de Sousa:
Tool-Assisted Specification and Verification of Typed Low-Level Languages.
J. Autom. Reasoning 35(4): 295-354 (2005) |
| 52 | | Gilles Barthe:
A computational view of implicit coercions in type theory.
Mathematical Structures in Computer Science 15(5): 839-874 (2005) |
| 2004 |
|---|
| 51 | | Mariela Pavlova,
Gilles Barthe,
Lilian Burdy,
Marieke Huisman,
Jean-Louis Lanet:
Enforcing High-Level Security Properties for Applets.
CARDIS 2004: 1-16 |
| 50 | | Gilles Barthe,
Pedro R. D'Argenio,
Tamara Rezk:
Secure Information Flow by Self-Composition.
CSFW 2004: 100-114 |
| 49 | | Gilles Barthe,
Guillaume Dufay:
A Tool-Assisted Framework for Certified Bytecode Verification.
FASE 2004: 99-113 |
| 48 | | Gilles Barthe,
Leonor Prensa Nieto:
Formally verifying information flow type systems for concurrent and thread systems.
FMSE 2004: 13-22 |
| 47 | | Gilles Barthe,
Jan Cederquist,
Sabrina Tarento:
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model.
IJCAR 2004: 385-399 |
| 46 | | Gilles Barthe,
Sabrina Tarento:
A Machine-Checked Formalization of the Random Oracle Model.
TYPES 2004: 33-49 |
| 45 | | Gilles Barthe,
Amitabh Basu,
Tamara Rezk:
Security Types Preserving Compilation: (Extended Abstract).
VMCAI 2004: 2-15 |
| 44 | | 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) |
| 43 | | Gilles Barthe,
Maria João Frade,
E. Giménez,
Luis Pinto,
Tarmo Uustalu:
Type-based termination of recursive definitions.
Mathematical Structures in Computer Science 14(1): 97-141 (2004) |
| 2003 |
|---|
| 42 | | Gilles Barthe,
Horatiu Cirstea,
Claude Kirchner,
Luigi Liquori:
Pure patterns type systems.
POPL 2003: 250-261 |
| 41 | | Gilles Barthe,
Sorin Stratulat:
Validation of the JavaCard Platform with Implicit Induction Techniques.
RTA 2003: 337-351 |
| 40 | | Gilles Barthe,
Venanzio Capretta,
Olivier Pons:
Setoids in type theory.
J. Funct. Program. 13(2): 261-293 (2003) |
| 2002 |
|---|
| 39 | | Gilles Barthe,
Peter Dybjer,
Luis Pinto,
João Saraiva:
Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures
Springer 2002 |
| 38 | | Gilles Barthe,
Pierre Courtieu,
Guillaume Dufay,
Simão Melo de Sousa:
Tool-Assisted Specification and Verification of the JavaCard Platform.
AMAST 2002: 41-59 |
| 37 | | Gilles Barthe,
Dilian Gurov,
Marieke Huisman:
Compositional Verification of Secure Applet Interactions.
FASE 2002: 15-32 |
| 36 | | Gilles Barthe,
Tarmo Uustalu:
CPS translating inductive and coinductive types.
PEPM 2002: 131-142 |
| 35 | | Gilles Barthe,
Pierre Courtieu:
Efficient Reasoning about Executable Specifications in Coq.
TPHOLs 2002: 31-46 |
| 34 | | 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 |
| 33 | | Gilles Barthe,
Peter Thiemann:
Preface.
Electr. Notes Theor. Comput. Sci. 75: (2002) |
| 2001 |
|---|
| 32 | | Gilles Barthe,
Guillaume Dufay,
Marieke Huisman,
Simão Melo de Sousa:
Jakarta: A Toolset for Reasoning about JavaCard.
E-smart 2001: 2-18 |
| 31 | | 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 |
| 30 | | Gilles Barthe,
Olivier Pons:
Type Isomorphisms and Proof Reuse in Dependent Type Theory.
FoSSaCS 2001: 57-71 |
| 29 | | Gilles Barthe,
John Hatcliff,
Morten Heine Sørensen:
An induction principle for pure type systems.
Theor. Comput. Sci. 266(1-2): 773-818 (2001) |
| 28 | | 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) |
| 2000 |
|---|
| 27 | | Gilles Barthe,
Thierry Coquand:
An Introduction to Dependent Type Theory.
APPSEM 2000: 1-41 |
| 26 | | Gilles Barthe,
Femke van Raamsdonk:
Constructor Subtyping in the Calculus of Inductive Constructions.
FoSSaCS 2000: 17-34 |
| 25 | | Gilles Barthe,
Bernard P. Serpette:
Static Reduction Analysis for Imperative Object Oriented Languages.
LPAR 2000: 344-361 |
| 24 | | Gilles Barthe,
Morten Heine Sørensen:
Domain-free pure type systems.
J. Funct. Program. 10(5): 417-452 (2000) |
| 1999 |
|---|
| 23 | | Gilles Barthe,
Maria João Frade:
Constructor Subtyping.
ESOP 1999: 109-127 |
| 22 | | Gilles Barthe:
Expanding the Cube.
FoSSaCS 1999: 90-103 |
| 21 | | Gilles Barthe,
Bernard P. Serpette:
Partial Evaluation and Non-inference for Object Calculi.
Fuji International Symposium on Functional and Logic Programming 1999: 53-67 |
| 20 | | Gilles Barthe,
John Hatcliff,
Morten Heine Sørensen:
CPS Translations and Applications: The Cube and Beyond.
Higher-Order and Symbolic Computation 12(2): 125-170 (1999) |
| 19 | | Gilles Barthe:
Order-Sorted Inductive Types.
Inf. Comput. 149(1): 42-76 (1999) |
| 18 | | Gilles Barthe:
Type-checking injective pure type systems.
J. Funct. Program. 9(6): 685-698 (1999) |
| 1998 |
|---|
| 17 | | Gilles Barthe:
Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion.
CSL 1998: 241-259 |
| 16 | | Gilles Barthe:
The Relevance of Proof-Irrelevance.
ICALP 1998: 755-768 |
| 15 | | Gilles Barthe:
The Semi-Full Closure of Pure Type Systems.
MFCS 1998: 316-325 |
| 1997 |
|---|
| 14 | | Gilles Barthe,
Femke van Raamsdonk:
Termination of Algebraic Type Systems: The Syntactic Approach.
ALP/HOA 1997: 174-193 |
| 13 | | Gilles Barthe,
Fairouz Kamareddine,
Alejandro Ríos:
Explicit Substitutions for the Lambda-Calculus.
ALP/HOA 1997: 209-223 |
| 12 | | Gilles Barthe,
Morten Heine Sørensen:
Domain-Free Pure Type Systems.
LFCS 1997: 9-20 |
| 11 | | Gilles Barthe,
John Hatcliff,
Morten Heine Sørensen:
Reflections on Reflections.
PLILP 1997: 241-258 |
| 10 | | Gilles Barthe,
John Hatcliff,
Peter Thiemann:
Monadic Type Systems: Pure Type Systems for Impure Settings.
Electr. Notes Theor. Comput. Sci. 10: (1997) |
| 9 | | Gilles Barthe,
John Hatcliff,
Morten Heine Sørensen:
A notion of classical pure type system.
Electr. Notes Theor. Comput. Sci. 6: 4-59 (1997) |
| 1996 |
|---|
| 8 | | Gilles Barthe,
Paul-André Melliès:
On the Subject Reduction Property for Algebraic Type Systems.
CSL 1996: 34-57 |
| 7 | | Gilles Barthe,
Hugo Elbers:
Towards Lean Proof Checking.
DISCO 1996: 61-62 |
| 1995 |
|---|
| 6 | | Gilles Barthe,
Herman Geuvers:
Congruence Types.
CSL 1995: 36-51 |
| 5 | | Gilles Barthe:
A Simple Abstract Semantics for Equational Theories.
FCT 1995: 126-135 |
| 4 | | Gilles Barthe,
Herman Geuvers:
Modular Properties of Algebraic Type Systems.
HOA 1995: 37-56 |
| 3 | | Gilles Barthe:
Extensions of Pure Type Systems.
TLCA 1995: 16-31 |
| 2 | | Gilles Barthe:
Implicit Coercions in Type Systems.
TYPES 1995: 1-15 |
| 1 | | Gilles Barthe,
Mark Ruys,
Henk Barendregt:
A Two-Level Approach Towards Lean Proof-Checking.
TYPES 1995: 16-35 |
