The SCEAS System
Navigation Menu
Introduction
Collection Based
Clustering
Ranking
Paper Based
Journals
Conferences
DB Status
Statistics
Search

Search the dblp DataBase

Title:
Author:
Gilles Barthe: [Publications] [Author Rank by year] [Co-authors] [Prefers] [Cites] [Cited by]

Publications of Author

  1. Gilles Barthe, Thierry Coquand
    An Introduction to Dependent Type Theory. [Citation Graph (0, 0)][DBLP]
    APPSEM, 2000, pp:1-41 [Conf]
  2. Gilles Barthe, Fairouz Kamareddine, Alejandro Ríos
    Explicit Substitutions for the Lambda-Calculus. [Citation Graph (0, 0)][DBLP]
    ALP/HOA, 1997, pp:209-223 [Conf]
  3. Gilles Barthe, Femke van Raamsdonk
    Termination of Algebraic Type Systems: The Syntactic Approach. [Citation Graph (0, 0)][DBLP]
    ALP/HOA, 1997, pp:174-193 [Conf]
  4. Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa
    Tool-Assisted Specification and Verification of the JavaCard Platform. [Citation Graph (0, 0)][DBLP]
    AMAST, 2002, pp:41-59 [Conf]
  5. Gilles Barthe, Jan Cederquist, Sabrina Tarento
    A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. [Citation Graph (0, 0)][DBLP]
    IJCAR, 2004, pp:385-399 [Conf]
  6. Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet
    Enforcing High-Level Security Properties for Applets. [Citation Graph (0, 0)][DBLP]
    CARDIS, 2004, pp:1-16 [Conf]
  7. Gilles Barthe, Leonor Prensa Nieto
    Formally verifying information flow type systems for concurrent and thread systems. [Citation Graph (0, 0)][DBLP]
    FMSE, 2004, pp:13-22 [Conf]
  8. Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk
    Secure Information Flow by Self-Composition. [Citation Graph (0, 0)][DBLP]
    CSFW, 2004, pp:100-114 [Conf]
  9. Gilles Barthe, Herman Geuvers
    Congruence Types. [Citation Graph (0, 0)][DBLP]
    CSL, 1995, pp:36-51 [Conf]
  10. Gilles Barthe, Paul-André Melliès
    On the Subject Reduction Property for Algebraic Type Systems. [Citation Graph (0, 0)][DBLP]
    CSL, 1996, pp:34-57 [Conf]
  11. Gilles Barthe
    Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion. [Citation Graph (0, 0)][DBLP]
    CSL, 1998, pp:241-259 [Conf]
  12. Gilles Barthe, Hugo Elbers
    Towards Lean Proof Checking. [Citation Graph (0, 0)][DBLP]
    DISCO, 1996, pp:61-62 [Conf]
  13. Gilles Barthe, Guillaume Dufay, Marieke Huisman, Simão Melo de Sousa
    Jakarta: A Toolset for Reasoning about JavaCard. [Citation Graph (0, 0)][DBLP]
    E-smart, 2001, pp:2-18 [Conf]
  14. Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard P. Serpette, Simão Melo de Sousa
    A Formal Executable Semantics of the JavaCard Platform. [Citation Graph (0, 0)][DBLP]
    ESOP, 2001, pp:302-319 [Conf]
  15. Gilles Barthe, Maria João Frade
    Constructor Subtyping. [Citation Graph (0, 0)][DBLP]
    ESOP, 1999, pp:109-127 [Conf]
  16. Gilles Barthe, Guillaume Dufay
    A Tool-Assisted Framework for Certified Bytecode Verification. [Citation Graph (0, 0)][DBLP]
    FASE, 2004, pp:99-113 [Conf]
  17. Gilles Barthe, Dilian Gurov, Marieke Huisman
    Compositional Verification of Secure Applet Interactions. [Citation Graph (0, 0)][DBLP]
    FASE, 2002, pp:15-32 [Conf]
  18. Gilles Barthe
    A Simple Abstract Semantics for Equational Theories. [Citation Graph (0, 0)][DBLP]
    FCT, 1995, pp:126-135 [Conf]
  19. Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu
    Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant. [Citation Graph (0, 0)][DBLP]
    FLOPS, 2006, pp:114-129 [Conf]
  20. Gilles Barthe, Bernard P. Serpette
    Partial Evaluation and Non-inference for Object Calculi. [Citation Graph (0, 0)][DBLP]
    Fuji International Symposium on Functional and Logic Programming, 1999, pp:53-67 [Conf]
  21. Gilles Barthe, Guillaume Dufay
    Formal Methods for Smartcard Security. [Citation Graph (0, 0)][DBLP]
    FOSAD, 2005, pp:133-177 [Conf]
  22. Gilles Barthe
    Expanding the Cube. [Citation Graph (0, 0)][DBLP]
    FoSSaCS, 1999, pp:90-103 [Conf]
  23. Gilles Barthe, Olivier Pons
    Type Isomorphisms and Proof Reuse in Dependent Type Theory. [Citation Graph (0, 0)][DBLP]
    FoSSaCS, 2001, pp:57-71 [Conf]
  24. Gilles Barthe, Femke van Raamsdonk
    Constructor Subtyping in the Calculus of Inductive Constructions. [Citation Graph (0, 0)][DBLP]
    FoSSaCS, 2000, pp:17-34 [Conf]
  25. Gilles Barthe, Herman Geuvers
    Modular Properties of Algebraic Type Systems. [Citation Graph (0, 0)][DBLP]
    HOA, 1995, pp:37-56 [Conf]
  26. Gilles Barthe
    The Relevance of Proof-Irrelevance. [Citation Graph (0, 0)][DBLP]
    ICALP, 1998, pp:755-768 [Conf]
  27. Gilles Barthe, Tamara Rezk, Ando Saabas
    Proof Obligations Preserving Compilation. [Citation Graph (0, 0)][DBLP]
    Formal Aspects in Security and Trust, 2005, pp:112-126 [Conf]
  28. Gilles Barthe, Morten Heine Sørensen
    Domain-Free Pure Type Systems. [Citation Graph (0, 0)][DBLP]
    LFCS, 1997, pp:9-20 [Conf]
  29. Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
    CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. [Citation Graph (0, 0)][DBLP]
    LPAR, 2006, pp:257-271 [Conf]
  30. Gilles Barthe, Bernard P. Serpette
    Static Reduction Analysis for Imperative Object Oriented Languages. [Citation Graph (0, 0)][DBLP]
    LPAR, 2000, pp:344-361 [Conf]
  31. Gilles Barthe
    The Semi-Full Closure of Pure Type Systems. [Citation Graph (0, 0)][DBLP]
    MFCS, 1998, pp:316-325 [Conf]
  32. Gilles Barthe, Tarmo Uustalu
    CPS translating inductive and coinductive types. [Citation Graph (0, 0)][DBLP]
    PEPM, 2002, pp:131-142 [Conf]
  33. Gilles Barthe, John Hatcliff, Morten Heine Sørensen
    Reflections on Reflections. [Citation Graph (0, 0)][DBLP]
    PLILP, 1997, pp:241-258 [Conf]
  34. Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori
    Pure patterns type systems. [Citation Graph (0, 0)][DBLP]
    POPL, 2003, pp:250-261 [Conf]
  35. Gilles Barthe, Sorin Stratulat
    Validation of the JavaCard Platform with Implicit Induction Techniques. [Citation Graph (0, 0)][DBLP]
    RTA, 2003, pp:337-351 [Conf]
  36. Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk
    Certificate Translation for Optimizing Compilers. [Citation Graph (0, 0)][DBLP]
    SAS, 2006, pp:301-317 [Conf]
  37. Gilles Barthe, Mariela Pavlova, Gerardo Schneider
    Precise Analysis of Memory Consumption using Program Logics. [Citation Graph (0, 0)][DBLP]
    SEFM, 2005, pp:86-95 [Conf]
  38. Gilles Barthe, Tamara Rezk, David A. Naumann
    Deriving an Information Flow Checker and Certifying Compiler for Java. [Citation Graph (0, 0)][DBLP]
    S&P, 2006, pp:230-242 [Conf]
  39. Gilles Barthe
    Extensions of Pure Type Systems. [Citation Graph (0, 0)][DBLP]
    TLCA, 1995, pp:16-31 [Conf]
  40. Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
    Practical Inference for Type-Based Termination in a Polymorphic Setting. [Citation Graph (0, 0)][DBLP]
    TLCA, 2005, pp:71-85 [Conf]
  41. Gilles Barthe, Tamara Rezk
    Non-interference for a JVM-like language. [Citation Graph (0, 0)][DBLP]
    TLDI, 2005, pp:103-112 [Conf]
  42. Gilles Barthe, Pierre Courtieu
    Efficient Reasoning about Executable Specifications in Coq. [Citation Graph (0, 0)][DBLP]
    TPHOLs, 2002, pp:31-46 [Conf]
  43. Gilles Barthe
    Implicit Coercions in Type Systems. [Citation Graph (0, 0)][DBLP]
    TYPES, 1995, pp:1-15 [Conf]
  44. Gilles Barthe, Mark Ruys, Henk Barendregt
    A Two-Level Approach Towards Lean Proof-Checking. [Citation Graph (0, 0)][DBLP]
    TYPES, 1995, pp:16-35 [Conf]
  45. Gilles Barthe, Sabrina Tarento
    A Machine-Checked Formalization of the Random Oracle Model. [Citation Graph (0, 0)][DBLP]
    TYPES, 2004, pp:33-49 [Conf]
  46. Gilles Barthe, Amitabh Basu, Tamara Rezk
    Security Types Preserving Compilation: (Extended Abstract). [Citation Graph (0, 0)][DBLP]
    VMCAI, 2004, pp:2-15 [Conf]
  47. Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa
    A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines. [Citation Graph (0, 0)][DBLP]
    VMCAI, 2002, pp:32-45 [Conf]
  48. Gilles Barthe, John Hatcliff, Morten Heine Sørensen
    A notion of classical pure type system. [Citation Graph (0, 0)][DBLP]
    Electr. Notes Theor. Comput. Sci., 1997, v:6, n:, pp:4-59 [Journal]
  49. Gilles Barthe, John Hatcliff, Peter Thiemann
    Monadic Type Systems: Pure Type Systems for Impure Settings. [Citation Graph (0, 0)][DBLP]
    Electr. Notes Theor. Comput. Sci., 1997, v:10, n:, pp:- [Journal]
  50. Gilles Barthe, Tamara Rezk, Martijn Warnier
    Preventing Timing Leaks Through Transactional Branching Instructions. [Citation Graph (0, 0)][DBLP]
    Electr. Notes Theor. Comput. Sci., 2006, v:153, n:2, pp:33-55 [Journal]
  51. Gilles Barthe, Peter Thiemann
    Preface. [Citation Graph (0, 0)][DBLP]
    Electr. Notes Theor. Comput. Sci., 2002, v:75, n:, pp:- [Journal]
  52. Gilles Barthe
    Order-Sorted Inductive Types. [Citation Graph (0, 0)][DBLP]
    Inf. Comput., 1999, v:149, n:1, pp:42-76 [Journal]
  53. Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa
    Tool-Assisted Specification and Verification of Typed Low-Level Languages. [Citation Graph (0, 0)][DBLP]
    J. Autom. Reasoning, 2005, v:35, n:4, pp:295-354 [Journal]
  54. Gilles Barthe
    Type-checking injective pure type systems. [Citation Graph (0, 0)][DBLP]
    J. Funct. Program., 1999, v:9, n:6, pp:685-698 [Journal]
  55. Gilles Barthe, Venanzio Capretta, Olivier Pons
    Setoids in type theory. [Citation Graph (0, 0)][DBLP]
    J. Funct. Program., 2003, v:13, n:2, pp:261-293 [Journal]
  56. Gilles Barthe, Peter Dybjer, Peter Thiemann
    Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming. [Citation Graph (0, 0)][DBLP]
    J. Funct. Program., 2004, v:14, n:1, pp:1-2 [Journal]
  57. Gilles Barthe, Morten Heine Sørensen
    Domain-free pure type systems. [Citation Graph (0, 0)][DBLP]
    J. Funct. Program., 2000, v:10, n:5, pp:417-452 [Journal]
  58. Gilles Barthe, Thierry Coquand
    Remarks on the equational theory of non-normalizing pure type systems. [Citation Graph (0, 0)][DBLP]
    J. Funct. Program., 2006, v:16, n:2, pp:137-155 [Journal]
  59. Gilles Barthe, John Hatcliff, Morten Heine Sørensen
    CPS Translations and Applications: The Cube and Beyond. [Citation Graph (0, 0)][DBLP]
    Higher-Order and Symbolic Computation, 1999, v:12, n:2, pp:125-170 [Journal]
  60. Gilles Barthe, Maria João Frade, E. Giménez, Luis Pinto, Tarmo Uustalu
    Type-based termination of recursive definitions. [Citation Graph (0, 0)][DBLP]
    Mathematical Structures in Computer Science, 2004, v:14, n:1, pp:97-141 [Journal]
  61. Gilles Barthe, John Hatcliff, Morten Heine Sørensen
    An induction principle for pure type systems. [Citation Graph (0, 0)][DBLP]
    Theor. Comput. Sci., 2001, v:266, n:1-2, pp:773-818 [Journal]
  62. Gilles Barthe, John Hatcliff, Morten Heine Sørensen
    Weak normalization implies strong normalization in a class of non-dependent pure type systems. [Citation Graph (0, 0)][DBLP]
    Theor. Comput. Sci., 2001, v:269, n:1-2, pp:317-361 [Journal]
  63. Gilles Barthe, David Pichardie, Tamara Rezk
    A Certified Lightweight Non-interference Java Bytecode Verifier. [Citation Graph (0, 0)][DBLP]
    ESOP, 2007, pp:125-140 [Conf]
  64. Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld
    Security of Multithreaded Programs by Compilation. [Citation Graph (0, 0)][DBLP]
    ESORICS, 2007, pp:2-18 [Conf]

  65. Certified Reasoning in Memory Hierarchies. [Citation Graph (, )][DBLP]


  66. Preservation of Proof Obligations from Java to the Java Virtual Machine. [Citation Graph (, )][DBLP]


  67. Certificate Translation. [Citation Graph (, )][DBLP]


  68. Tractable Enforcement of Declassification Policies. [Citation Graph (, )][DBLP]


  69. A Machine-Checked Formalization of Sigma-Protocols. [Citation Graph (, )][DBLP]


  70. Robustness Guarantees for Anonymity. [Citation Graph (, )][DBLP]


  71. Type-Based Termination with Sized Products. [Citation Graph (, )][DBLP]


  72. 07091 Executive Summary - Mobility, Ubiquity and Security. [Citation Graph (, )][DBLP]


  73. 07091 Abstracts Collection - Mobility, Ubiquity and Security. [Citation Graph (, )][DBLP]


  74. Certificate Translation in Abstract Interpretation. [Citation Graph (, )][DBLP]


  75. A Functional Framework for Result Checking. [Citation Graph (, )][DBLP]


  76. The MOBIUS Proof Carrying Code Infrastructure. [Citation Graph (, )][DBLP]


  77. JACK - A Tool for Validation of Security and Behaviour of Java Applications. [Citation Graph (, )][DBLP]


  78. An Introduction to Certificate Translation. [Citation Graph (, )][DBLP]


  79. Implementing a Direct Method for Certificate Translation. [Citation Graph (, )][DBLP]


  80. Formal Certification of ElGamal Encryption. [Citation Graph (, )][DBLP]


  81. Formal certification of code-based cryptographic proofs. [Citation Graph (, )][DBLP]


  82. Preservation of Proof Pbligations for Hybrid Verification Methods. [Citation Graph (, )][DBLP]


  83. Formally Certifying the Security of Digital Signature Schemes. [Citation Graph (, )][DBLP]


  84. MOBIUS: Mobility, Ubiquity, Security. [Citation Graph (, )][DBLP]


  85. Certificate translation for specification-preserving advices. [Citation Graph (, )][DBLP]


  86. A Tutorial on Type-Based Termination. [Citation Graph (, )][DBLP]


  87. Programming Language Techniques for Cryptographic Proofs. [Citation Graph (, )][DBLP]


  88. Security types preserving compilation. [Citation Graph (, )][DBLP]


Search in 0.017secs, Finished in 0.467secs
NOTICE1
System may not be available sometimes or not working properly, since it is still in development with continuous upgrades
NOTICE2
The rankings that are presented on this page should NOT be considered as formal since the citation info is incomplete in DBLP
 
Introduction Collection Based Clustering Ranking Paper Based Journals Conferences DB Status Statistics Search
System created by asidirop@csd.auth.gr [http://users.auth.gr/~asidirop/] © 2002
for Data Engineering Laboratory, Department of Informatics, Aristotle University © 2002