dblp.uni-trier.dewww.uni-trier.de

Gilles Barthe Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo
Home Page

*2009
92EEAlessandro Aldini, Gilles Barthe, Roberto Gorrieri: Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures Springer 2009
91EESantiago 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
90EEGilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin: Formal certification of code-based cryptographic proofs. POPL 2009: 90-101
89EEGilles 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
86EEGilles Barthe, César Kunz, Jorge Luis Sacchini: Certified Reasoning in Memory Hierarchies. APLAS 2008: 75-90
85EEGilles Barthe, Salvador Cavadini, Tamara Rezk: Tractable Enforcement of Declassification Policies. CSF 2008: 83-97
84EEGilles Barthe, Benjamin Grégoire, Colin Riba: Type-Based Termination with Sized Products. CSL 2008: 493-507
83EEGilles Barthe, César Kunz: Certificate Translation in Abstract Interpretation. ESOP 2008: 368-382
82EEGilles Barthe, César Kunz: Certificate translation for specification-preserving advices. FOAL 2008: 9-18
81EEGilles Barthe, César Kunz: An Introduction to Certificate Translation. FOSAD 2008: 51-95
80EEGilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin: Formal Certification of ElGamal Encryption. Formal Aspects in Security and Trust 2008: 1-19
79EEGilles Barthe, Benjamin Grégoire, Mariela Pavlova: Preservation of Proof Obligations from Java to the Java Virtual Machine. IJCAR 2008: 83-99
78EEGilles Barthe, Benjamin Grégoire, Colin Riba: A Tutorial on Type-Based Termination. LerNet ALFA Summer School 2008: 100-152
77EEGilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese: Preservation of Proof Pbligations for Hybrid Verification Methods. SEFM 2008: 127-136
76EEGilles 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
74EEGilles Barthe, David Pichardie, Tamara Rezk: A Certified Lightweight Non-interference Java Bytecode Verifier. ESOP 2007: 125-140
73EEGilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld: Security of Multithreaded Programs by Compilation. ESORICS 2007: 2-18
72EEGilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie: The MOBIUS Proof Carrying Code Infrastructure. FMCO 2007: 1-24
71EEGilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld: 07091 Abstracts Collection - Mobility, Ubiquity and Security. Mobility, Ubiquity and Security 2007
70EEGilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld: 07091 Executive Summary - Mobility, Ubiquity and Security. Mobility, Ubiquity and Security 2007
69EEGilles 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
67EEGilles 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
66EEGilles 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
65EEGilles 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
64EEGilles Barthe, Benjamin Grégoire, Fernando Pastawski: CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. LPAR 2006: 257-271
63EEGilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk: Certificate Translation for Optimizing Compilers. SAS 2006: 301-317
62EEGilles 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
61EEGilles Barthe, Tamara Rezk, Martijn Warnier: Preventing Timing Leaks Through Transactional Branching Instructions. Electr. Notes Theor. Comput. Sci. 153(2): 33-55 (2006)
60EEGilles 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
58EEGilles Barthe, Guillaume Dufay: Formal Methods for Smartcard Security. FOSAD 2005: 133-177
57EEGilles Barthe, Tamara Rezk, Ando Saabas: Proof Obligations Preserving Compilation. Formal Aspects in Security and Trust 2005: 112-126
56EEGilles Barthe, Mariela Pavlova, Gerardo Schneider: Precise Analysis of Memory Consumption using Program Logics. SEFM 2005: 86-95
55EEGilles Barthe, Benjamin Grégoire, Fernando Pastawski: Practical Inference for Type-Based Termination in a Polymorphic Setting. TLCA 2005: 71-85
54EEGilles Barthe, Tamara Rezk: Non-interference for a JVM-like language. TLDI 2005: 103-112
53EEGilles 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)
52EEGilles 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
50EEGilles Barthe, Pedro R. D'Argenio, Tamara Rezk: Secure Information Flow by Self-Composition. CSFW 2004: 100-114
49EEGilles Barthe, Guillaume Dufay: A Tool-Assisted Framework for Certified Bytecode Verification. FASE 2004: 99-113
48EEGilles Barthe, Leonor Prensa Nieto: Formally verifying information flow type systems for concurrent and thread systems. FMSE 2004: 13-22
47EEGilles Barthe, Jan Cederquist, Sabrina Tarento: A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. IJCAR 2004: 385-399
46EEGilles Barthe, Sabrina Tarento: A Machine-Checked Formalization of the Random Oracle Model. TYPES 2004: 33-49
45EEGilles Barthe, Amitabh Basu, Tamara Rezk: Security Types Preserving Compilation: (Extended Abstract). VMCAI 2004: 2-15
44EEGilles 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)
43EEGilles 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
42EEGilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori: Pure patterns type systems. POPL 2003: 250-261
41EEGilles Barthe, Sorin Stratulat: Validation of the JavaCard Platform with Implicit Induction Techniques. RTA 2003: 337-351
40EEGilles 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
38EEGilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa: Tool-Assisted Specification and Verification of the JavaCard Platform. AMAST 2002: 41-59
37EEGilles Barthe, Dilian Gurov, Marieke Huisman: Compositional Verification of Secure Applet Interactions. FASE 2002: 15-32
36EEGilles Barthe, Tarmo Uustalu: CPS translating inductive and coinductive types. PEPM 2002: 131-142
35EEGilles Barthe, Pierre Courtieu: Efficient Reasoning about Executable Specifications in Coq. TPHOLs 2002: 31-46
34EEGilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa: A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. VMCAI 2002: 32-45
33EEGilles Barthe, Peter Thiemann: Preface. Electr. Notes Theor. Comput. Sci. 75: (2002)
2001
32EEGilles Barthe, Guillaume Dufay, Marieke Huisman, Simão Melo de Sousa: Jakarta: A Toolset for Reasoning about JavaCard. E-smart 2001: 2-18
31EEGilles 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
30EEGilles Barthe, Olivier Pons: Type Isomorphisms and Proof Reuse in Dependent Type Theory. FoSSaCS 2001: 57-71
29EEGilles Barthe, John Hatcliff, Morten Heine Sørensen: An induction principle for pure type systems. Theor. Comput. Sci. 266(1-2): 773-818 (2001)
28EEGilles 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
27EEGilles Barthe, Thierry Coquand: An Introduction to Dependent Type Theory. APPSEM 2000: 1-41
26EEGilles Barthe, Femke van Raamsdonk: Constructor Subtyping in the Calculus of Inductive Constructions. FoSSaCS 2000: 17-34
25EEGilles 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
23EEGilles 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
17EEGilles Barthe: Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion. CSL 1998: 241-259
16EEGilles Barthe: The Relevance of Proof-Irrelevance. ICALP 1998: 755-768
15EEGilles Barthe: The Semi-Full Closure of Pure Type Systems. MFCS 1998: 316-325
1997
14EEGilles Barthe, Femke van Raamsdonk: Termination of Algebraic Type Systems: The Syntactic Approach. ALP/HOA 1997: 174-193
13EEGilles 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
11EEGilles Barthe, John Hatcliff, Morten Heine Sørensen: Reflections on Reflections. PLILP 1997: 241-258
10EEGilles Barthe, John Hatcliff, Peter Thiemann: Monadic Type Systems: Pure Type Systems for Impure Settings. Electr. Notes Theor. Comput. Sci. 10: (1997)
9EEGilles Barthe, John Hatcliff, Morten Heine Sørensen: A notion of classical pure type system. Electr. Notes Theor. Comput. Sci. 6: 4-59 (1997)
1996
8EEGilles Barthe, Paul-André Melliès: On the Subject Reduction Property for Algebraic Type Systems. CSL 1996: 34-57
7EEGilles Barthe, Hugo Elbers: Towards Lean Proof Checking. DISCO 1996: 61-62
1995
6EEGilles 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
2EEGilles Barthe: Implicit Coercions in Type Systems. TYPES 1995: 1-15
1EEGilles Barthe, Mark Ruys, Henk Barendregt: A Two-Level Approach Towards Lean Proof-Checking. TYPES 1995: 16-35

Coauthor Index

1Alessandro Aldini [92]
2Hendrik Pieter Barendregt (Henk Barendregt) [1]
3Amitabh Basu [45]
4Santiago Zanella Béguelin [80] [90] [91]
5Lennart Beringer [62]
6Frank S. de Boer [87]
7Lilian Burdy [51] [59] [66]
8Venanzio Capretta [40]
9Salvador Cavadini [85]
10J. G. Cederquist (Jan Cederquist) [47]
11Julien Charles [66]
12Horatiu Cirstea [42]
13Thierry Coquand [27] [60]
14Pierre Courtieu [35] [38] [53]
15Pierre Crégut [62] [72]
16Pedro R. D'Argenio [50]
17Guillaume Dufay [31] [32] [34] [38] [49] [53] [58]
18Peter Dybjer [39] [44]
19Hugo Elbers [7]
20Julien Forest [67]
21Cédric Fournet [88]
22Maria João Frade [23] [43]
23Herman Geuvers [4] [6]
24E. Giménez [43]
25Roberto Gorrieri [92]
26Benjamin Grégoire [55] [62] [63] [64] [66] [68] [72] [78] [79] [80] [84] [89] [90] [91]
27Dilian Gurov [37]
28John Hatcliff [9] [10] [11] [20] [28] [29]
29Sylvain Heraud [80]
30Martin Hofmann [62]
31Marieke Huisman [32] [37] [51] [59] [66] [68]
32Line Jakubiec [31] [34]
33Thomas P. Jensen [72]
34Fairouz Kamareddine [13]
35Claude Kirchner [42]
36César Kunz [63] [77] [81] [82] [83] [86] [89]
37Jean-Louis Lanet [51] [59] [66] [68]
38Luigi Liquori [42]
39Heiko Mantel [70] [71] [75]
40Paul-André Melliès [8]
41Peter Müller [62] [70] [71] [75]
42Traian Muntean [59]
43Andrew C. Myers [70] [71] [75]
44David A. Naumann [65]
45Leonor Prensa Nieto [48] [69]
46Federico Olmedo [91]
47Fernando Pastawski [55] [64]
48Mariela Pavlova [51] [56] [66] [79]
49David Pichardie [67] [72] [74] [77]
50Luis Pinto [39] [43]
51Erik Poll [62]
52Olivier Pons [30] [40]
53Germán Puebla (German Puebla) [62]
54Femke van Raamsdonk [14] [26]
55Antoine Requet [66]
56Tamara Rezk [45] [50] [54] [57] [61] [63] [65] [73] [74] [85] [89]
57Colin Riba [78] [84]
58Alejandro Ríos [13]
59Alejandro Russo [73]
60Vlad Rusu [67]
61Mark Ruys [1]
62Ando Saabas [57]
63Andrei Sabelfeld [70] [71] [73] [75]
64Jorge Luis Sacchini [86]
65Julián Samborski-Forlese [77]
66João Saraiva [39]
67Gerardo Schneider [56]
68Bernard P. Serpette [21] [25] [31]
69Morten Heine Sørensen [9] [11] [12] [20] [24] [28] [29]
70Simão Melo de Sousa [31] [32] [34] [38] [53]
71Ian Stark [62]
72Sorin Stratulat [41]
73Sabrina Tarento [46] [47]
74Peter Thiemann [10] [33] [44]
75Tarmo Uustalu [36] [43]
76Eric Vétillard [62]
77Martijn Warnier [61]

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)