2009 | ||
---|---|---|
87 | EE | Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin: Formal certification of code-based cryptographic proofs. POPL 2009: 90-101 |
2008 | ||
86 | Gilles Barthe, Cédric Fournet: Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers Springer 2008 | |
85 | 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 | |
84 | EE | Gilles Barthe, César Kunz, Jorge Luis Sacchini: Certified Reasoning in Memory Hierarchies. APLAS 2008: 75-90 |
83 | EE | Gilles Barthe, Salvador Cavadini, Tamara Rezk: Tractable Enforcement of Declassification Policies. CSF 2008: 83-97 |
82 | EE | Gilles Barthe, Benjamin Grégoire, Colin Riba: Type-Based Termination with Sized Products. CSL 2008: 493-507 |
81 | EE | Gilles Barthe, César Kunz: Certificate Translation in Abstract Interpretation. ESOP 2008: 368-382 |
80 | EE | Gilles Barthe, César Kunz: Certificate translation for specification-preserving advices. FOAL 2008: 9-18 |
79 | EE | 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 |
78 | EE | Gilles Barthe, Benjamin Grégoire, Mariela Pavlova: Preservation of Proof Obligations from Java to the Java Virtual Machine. IJCAR 2008: 83-99 |
77 | EE | Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese: Preservation of Proof Pbligations for Hybrid Verification Methods. SEFM 2008: 127-136 |
76 | EE | 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 | EE | Gilles Barthe, David Pichardie, Tamara Rezk: A Certified Lightweight Non-interference Java Bytecode Verifier. ESOP 2007: 125-140 |
73 | EE | Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld: Security of Multithreaded Programs by Compilation. ESORICS 2007: 2-18 |
72 | EE | Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie: The MOBIUS Proof Carrying Code Infrastructure. FMCO 2007: 1-24 |
71 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | 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 | EE | Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk: Certificate Translation for Optimizing Compilers. SAS 2006: 301-317 |
62 | EE | 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 | EE | Gilles Barthe, Tamara Rezk, Martijn Warnier: Preventing Timing Leaks Through Transactional Branching Instructions. Electr. Notes Theor. Comput. Sci. 153(2): 33-55 (2006) |
60 | EE | 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 | EE | Gilles Barthe, Guillaume Dufay: Formal Methods for Smartcard Security. FOSAD 2005: 133-177 |
57 | EE | Gilles Barthe, Tamara Rezk, Ando Saabas: Proof Obligations Preserving Compilation. Formal Aspects in Security and Trust 2005: 112-126 |
56 | EE | Gilles Barthe, Mariela Pavlova, Gerardo Schneider: Precise Analysis of Memory Consumption using Program Logics. SEFM 2005: 86-95 |
55 | EE | Gilles Barthe, Benjamin Grégoire, Fernando Pastawski: Practical Inference for Type-Based Termination in a Polymorphic Setting. TLCA 2005: 71-85 |
54 | EE | Gilles Barthe, Tamara Rezk: Non-interference for a JVM-like language. TLDI 2005: 103-112 |
53 | EE | 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 | EE | 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 | EE | Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk: Secure Information Flow by Self-Composition. CSFW 2004: 100-114 |
49 | EE | Gilles Barthe, Guillaume Dufay: A Tool-Assisted Framework for Certified Bytecode Verification. FASE 2004: 99-113 |
48 | EE | Gilles Barthe, Leonor Prensa Nieto: Formally verifying information flow type systems for concurrent and thread systems. FMSE 2004: 13-22 |
47 | EE | Gilles Barthe, Jan Cederquist, Sabrina Tarento: A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. IJCAR 2004: 385-399 |
46 | EE | Gilles Barthe, Sabrina Tarento: A Machine-Checked Formalization of the Random Oracle Model. TYPES 2004: 33-49 |
45 | EE | Gilles Barthe, Amitabh Basu, Tamara Rezk: Security Types Preserving Compilation: (Extended Abstract). VMCAI 2004: 2-15 |
44 | EE | 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 | EE | 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 | EE | Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori: Pure patterns type systems. POPL 2003: 250-261 |
41 | EE | Gilles Barthe, Sorin Stratulat: Validation of the JavaCard Platform with Implicit Induction Techniques. RTA 2003: 337-351 |
40 | EE | 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 | EE | 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 | EE | Gilles Barthe, Dilian Gurov, Marieke Huisman: Compositional Verification of Secure Applet Interactions. FASE 2002: 15-32 |
36 | EE | Gilles Barthe, Tarmo Uustalu: CPS translating inductive and coinductive types. PEPM 2002: 131-142 |
35 | EE | Gilles Barthe, Pierre Courtieu: Efficient Reasoning about Executable Specifications in Coq. TPHOLs 2002: 31-46 |
34 | EE | 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 | EE | Gilles Barthe, Peter Thiemann: Preface. Electr. Notes Theor. Comput. Sci. 75: (2002) |
2001 | ||
32 | EE | Gilles Barthe, Guillaume Dufay, Marieke Huisman, Simão Melo de Sousa: Jakarta: A Toolset for Reasoning about JavaCard. E-smart 2001: 2-18 |
31 | EE | 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 | EE | Gilles Barthe, Olivier Pons: Type Isomorphisms and Proof Reuse in Dependent Type Theory. FoSSaCS 2001: 57-71 |
29 | EE | 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 | EE | 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 | EE | Gilles Barthe, Thierry Coquand: An Introduction to Dependent Type Theory. APPSEM 2000: 1-41 |
26 | EE | Gilles Barthe, Femke van Raamsdonk: Constructor Subtyping in the Calculus of Inductive Constructions. FoSSaCS 2000: 17-34 |
25 | EE | 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 | EE | 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 | EE | Gilles Barthe: The Relevance of Proof-Irrelevance. ICALP 1998: 755-768 |
15 | EE | 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 | EE | Gilles Barthe, John Hatcliff, Peter Thiemann: Monadic Type Systems: Pure Type Systems for Impure Settings. Electr. Notes Theor. Comput. Sci. 10: (1997) |
9 | EE | 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 | EE | Gilles Barthe: Implicit Coercions in Type Systems. TYPES 1995: 1-15 |
1 | EE | Gilles Barthe, Mark Ruys, Henk Barendregt: A Two-Level Approach Towards Lean Proof-Checking. TYPES 1995: 16-35 |