english version Toutes les publications de l'équipe
Publications - Gilles Barthe
[Format BibTeX]

[BK08a] G. Barthe and C. Kunz. Certificate translation for specification-preserving advices. In Proceedings of the Foundations of Aspect-Oriented Languages Workshop (FOAL), Brussels, Belgium, April 2008. ACM. [ bib | .pdf ]
[BK08b] G. Barthe and C. Kunz. Certificate translation in abstract interpretation. In Proceedings of the 17th European Symposium on Programming (ESOP), LNCS, Budapest, Hungary, March-April 2008. Springer-Verlag. [ bib | .pdf ]
[BGJB07] Gilles Barthe, Bejamin Grégoire, Romain Janvier, and Santiago Zanella Béguelin. A framework for language-based cryptographic proofs. Oct 2007. [ bib ]
[BBC+07] G. Barthe, L. Burdy, J. Charles, B. Grégoire, M. Huisman, J.-L. Lanet, M. Pavlova, and A. Requet. JACK: a tool for validation of security and behaviour of Java applications. In FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects, Lecture Notes in Computer Science. Springer-Verlag, 2007. To appear. [ bib | .pdf ]
[BGP06] G. Barthe, B. Grégoire, and F. Pastawski. Type-based termination of recursive definitions in the calculus of inductive constructions. In Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'06), Lecture Notes in Artificial Intelligence. Springer-Verlag, November 2006. To appear. [ bib | .pdf.gz | .ps.gz ]
[BGKR06] G. Barthe, B. Grégoire, C. Kunz, and T. Rezk. Certificate translation for optimizing compilers. In Proceedings of the 13th International Static Analysis Symposium (SAS), LNCS, Seoul, Korea, August 2006. Springer-Verlag. [ bib | .pdf ]
[BNR06b] G. Barthe, D. Naumann, and T. Rezk. Deriving an information flow checker and certifying compiler for Java. In Proceedings of Symposium of Security and Privacy'06. IEEE Press, 2006. [ bib | .ps ]
[BNR06a] G. Barthe, D. Naumann, and T. Rezk. Deriving an information flow checker and certifying compiler for Java, 2006. To appear. [ bib ]
[BPR06] G. Barthe, D. Pichardie, and T. Rezk. Deriving an information flow checker for the JVM. Technical report, INRIA, 2006. [ bib ]
[BFPR06] G. Barthe, J. Forest, D. Pichardie, and V. Rusu. Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In M. Hagiya and P. Wadler, editors, Proceedings of FLOPS'06, volume 3945 of Lecture Notes in Computer Science, pages 114-129. Springer-Verlag, 2006. [ bib | .pdf | .ps.gz ]
[BDR06] G. Barthe, P. D'Argenio, and T. Rezk. Secure Information Flow by Self-Composition. Technical report, INRIA, 2006. [ bib ]
[BBC+06] Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, and Eric Vétillard. Mobius: Mobility, ubiquity, security. objectives and progress report. In TGC 2006: Proceedings of the second symposium on Trustworthy Global Computing, LNCS. Springer-Verlag, 2006. [ bib | .pdf ]
[BPS05] G. Barthe, M. Pavlova, and G. Schneider. Precise analysis of memory consumption using program logics. In B. Aichernig and B. Beckert, editors, Proceedings of SEFM'05, pages 86-95, Koblenz, Germany, September 2005. IEEE Computer Society. [ bib | .pdf ]
[BGP05] G. Barthe, B. Grégoire, and F. Pastawski. Practical inference for typed-based termination in a polymorphic setting. In P. Urzyczyn, editor, Proceedings of TLCA'05, volume 3641 of Lecture Notes in Computer Science, pages 71-85, Nara, Japan, April 2005. Springer-Verlag. [ bib | .ps.gz ]
[BD05] G. Barthe and G. Dufay. Formal methods for smartcard security. In A. Aldini, R. Gorrieri, and F. Martinelli, editors, Proceedings of FOSAD'05, volume 3655 of Lecture Notes in Computer Science, pages 133-177. Springer-Verlag, 2005. [ bib | .pdf ]
[BRS05] G. Barthe, T. Rezk, and A. Saabas. Proof obligations preserving compilation. In R. Gorrieri, F. Martinelli, P. Ryan, and S. Schneider, editors, Proceedings of FAST'05, volume 3866 of Lecture Notes in Computer Science, pages 112-126. Springer-Verlag, 2005. [ bib | .pdf ]
[BT05] G. Barthe and S. Tarento. A machine-checked formalization of the random oracle model. In J.C. Filliâtre, C. Paulin-Mohring, and B. Werner, editors, Proceedings of TYPES'04, volume 3839 of Lecture Notes in Computer Science. Springer-Verlag, 2005. [ bib | .pdf ]
[BRW05] G. Barthe, T. Rezk, and M. Warnier. Preventing timing leaks through transactional branching instructions. In Proceedings of 3rd Workshop on Quantitative Aspects of Programming Languages (QAPL'05), Edinburgh, Scotland, 2005. Electronic Notes in Theoretical Computer Science. to appear. [ bib | .pdf ]
[BR05] G. Barthe and T. Rezk. Non-interference for a JVM-like language. In M. Fähndrich, editor, Proceedings of TLDI'05, pages 103-112, Long Beach, USA, January 2005. ACM Press. [ bib | .ps.gz ]
[Bar05] G. Barthe. Type isomorphisms and back-and-forth coercions in type theory. Mathematical Structures in Computer Science, 2005. [ bib ]
[BPN04] G. Barthe and L. Prensa-Nieto. Formally verifying information flow type systems for concurrent and thread systems. In M. Backes, D. Basin, and M. Waidner, editors, Proceedings of FMSE'04, pages 13-22, Washington D.C., USA, October 2004. ACM Press. [ bib | .ps.gz ]
[PBB+04] M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J.-L. Lanet. Enforcing high-level security properties for applets. In P. Paradinas and J.-J. Quisquater, editors, Proceedings of CARDIS'04, Toulouse, France, August 2004. Kluwer Academic Publishers. [ bib | .pdf ]
[BCT04] G. Barthe, J. Cederquist, and S. Tarento. A Machine-Checked Formalization of the Generic Model and the Random Oracle Model. In D. Basin and M. Rusinowitch, editors, Proceedings of IJCAR'04, volume 3097 of Lecture Notes in Computer Science, pages 385-399, Cork, Ireland, July 2004. Springer-Verlag. [ bib | .ps.gz ]
[BDR04] G. Barthe, P. D'Argenio, and T. Rezk. Secure Information Flow by Self-Composition. In R. Foccardi, editor, Proceedings of CSFW'04, pages 100-114, Pacific Grove,USA, June 2004. IEEE Press. [ bib | .ps.gz ]
[BD04] G. Barthe and G. Dufay. A Tool-Assisted Framework for Certified Bytecode Verification. In M. Wermelinger and T. Margaria-Steffen, editors, Proceedings of FASE'04, volume 2984 of Lecture Notes in Computer Science, pages 99-113, Barcelona, Spain, March 2004. Springer-Verlag. [ bib | .ps.gz ]
[BC04] G. Barthe and T. Coquand. On the equational theory of non-normalizing pure type systems. Journal of Functional Programming, 14(2):191-209, March 2004. [ bib | .ps.gz ]
[BFG+04] G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu. Type-based termination of recursive definitions. Mathematical Structures in Computer Science, 14:97-141, February 2004. [ bib | .ps.gz ]
[BBR04] G. Barthe, A. Basu, and T. Rezk. Security types preserving compilation. In B. Steffen and G. Levi, editors, Proceedings of VMCAI'04, volume 2934 of Lecture Notes in Computer Science, pages 2-15, Venice, Italy, January 2004. Springer-Verlag. [ bib | .ps.gz ]
[Bar04] G. Barthe. De la théorie des types à la vérification formelles des petits objets portables de sécurité. Habilitation à diriger des recherches, Université de Nice Sophia-Antipolis, 2004. [ bib ]
[BS03] G. Barthe and S. Stratulat. Using Implicit Induction Techniques for the Validation of the JavaCard Platform. In R. Nieuwenhuis, editor, Proceedings of RTA'03, volume 2706 of Lecture Notes in Computer Science, pages 337 - 351, Valencia, Spain, June 2003. Springer-Verlag. [ bib | .ps.gz ]
[BCP03] G. Barthe, V. Capretta, and O. Pons. Setoids in type theory. Journal of Functional Programming, 13:261-293, March 2003. [ bib ]
[BCKL03] G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori. Pure pattern type systems. In Proceedings of POPL'03, New Orleans, USA, January 2003. ACM Press. [ bib | .ps.gz ]
[PBB+03] M. Pavlova, G. Barthe, L. Burdy, M. Huisman, and J.-L. Lanet. Enforcing high-level security properties for applets. Technical Report RR-5061, INRIA, 2003. [ bib | .html ]
[BGH02] G. Barthe, D. Gurov, and M. Huisman. Compositional verification of secure applet interactions. In Fundamental Approaches to Software Engineering (FASE'02), volume 2306 of Lecture Notes in Computer Science, pages 15-32. Springer-Verlag, 2002. [ bib | .ps.gz ]
[BCDdS02] G. Barthe, P. Courtieu, G. Dufay, and S. Melo de Sousa. Tool-Assisted Specification and Verification of the JavaCard Platform. In H. Kirchner and C. Ringessein, editors, Proceedings of AMAST'02, volume 2422 of Lecture Notes in Computer Science, pages 41-59. Springer-Verlag, 2002. [ bib | .ps.gz ]
[BC02a] G. Barthe and T. Coquand. An Introduction to Dependent Type Theory. In G. Barthe, P. Dybjer, L. Pinto, and J. Saraiva, editors, Applied Semantics. Lecture Notes for the APPSEM Summer School, volume 2395 of Lecture Notes in Computer Science, pages 1-41. Springer-Verlag, 2002. [ bib | .ps.gz ]
[BC02b] G. Barthe and P. Courtieu. Efficient Reasoning about Executable Specifications in Coq. In V. Carreño, C. Muñoz, and S. Tahar, editors, Proceedings of TPHOLs'02, volume 2410 of Lecture Notes in Computer Science, pages 31-46. Springer-Verlag, 2002. [ bib | .ps.gz ]
[BDJdS02] G. Barthe, G. Dufay, L. Jakubiec, and S. Melo de Sousa. A formal correspondence between offensive and defensive JavaCard virtual machines. In A. Cortesi, editor, Proceedings of VMCAI'02, volume 2294 of Lecture Notes in Computer Science, pages 32-45. Springer-Verlag, 2002. [ bib | .ps.gz ]
[BU02] G. Barthe and T. Uustalu. Cps translating inductive and coinductive types. In P. Thiemann, editor, Proceedings of PEPM'02. ACM Press, 2002. [ bib | .ps.gz ]
[BHS01a] G. Barthe, J. Hatcliff, and M.H. Sørensen. Weak Normalization implies Strong Normalization in Generalized Non-Dependent Pure Type Systems. Theoretical Computer Science, 269(1-2):317-361, October 2001. [ bib ]
[BHS01b] G. Barthe, J. Hatcliff, and M.H.B. Sørensen. An induction principle for Pure Type Systems. Theoretical Computer Science, 266(1-2):773-818, September 2001. [ bib | .ps.gz ]
[BDHdS01] G. Barthe, G. Dufay, M. Huisman, and S. Melo de Sousa. Jakarta: a toolset to reason about the JavaCard platform. In I. Attali and T. Jensen, editors, Proceedings of e-SMART'01, volume 2140 of Lecture Notes in Computer Science, pages 2-18. Springer-Verlag, 2001. [ bib | .ps.gz ]
[BP01] G. Barthe and O. Pons. Type Isomorphisms and Proof Reuse in Dependent Type Theory. In F. Honsell and M. Miculan, editors, Proceedings of FOSSACS'01, volume 2030 of Lecture Notes in Computer Science, pages 57-71. Springer-Verlag, 2001. [ bib | .ps.gz ]
[BDJ+01] G. Barthe, G. Dufay, L. Jakubiec, B. Serpette, and S. Melo de Sousa. A Formal Executable Semantics of the JavaCard Platform. In D. Sands, editor, Proceedings of ESOP'01, volume 2028 of Lecture Notes in Computer Science, pages 302-319. Springer-Verlag, 2001. [ bib | .ps.gz ]
[BGH01] G. Barthe, D. Gurov, and M. Huisman. Compositional specification and verification of control flow based security properties of multi-application programs. In Workshop on Formal Techniques for Java Programs (FTfJP), 2001. [ bib | .ps.gz ]
[BS00b] G. Barthe and M.H. Sørensen. Domain-free pure type systems. Journal of Functional Programming, 10(5):417-452, September 2000. [ bib | .ps.gz ]
[BS00a] G. Barthe and B. Serpette. Static reduction analysis for imperative object oriented languages. In M. Parigot and A. Voronkov, editors, Proceedings of LPAR'00, volume 1955 of Lecture Notes in Computer Science, pages 344-361. Springer-Verlag, 2000. [ bib | .ps.gz ]
[BR00] G. Barthe and F. van Raamsdonk. Constructor subtyping in the calculus of inductive constructions. In J. Tuyrin, editor, Proceedings of FOSSACS'00, volume 1784 of Lecture Notes in Computer Science, pages 17-34. Springer-Verlag, 2000. [ bib | .ps.gz ]
[BHS99] G. Barthe, J. Hatcliff, and M.H. Sørensen. CPS-translations and applications: the cube and beyond. Higher-Order and Symbolic Computation, 12(2):125-170, September 1999. [ bib | .ps.gz ]
[Bar99c] G. Barthe. Order-sorted inductive types. Information and Computation, 149(1):42-76, February 1999. [ bib | .ps.gz ]
[BS99] G. Barthe and B. Serpette. Partial evaluation and non-interference for object calculi. In A. Middeldorp and T. Sato, editors, Proceedings of FLOPS'99, volume 1722 of Lecture Notes in Computer Science, pages 53-67. Springer-Verlag, 1999. [ bib | .ps.gz ]
[Bar99b] G. Barthe. Expanding the cube. In W. Thomas, editor, Proceedings of FOSSACS'99, volume 1578 of Lecture Notes in Computer Science, pages 90-103. Springer-Verlag, 1999. [ bib | .ps.gz ]
[BF99] G. Barthe and M.J. Frade. Constructor subtyping. In D. Swiestra, editor, Proceedings of ESOP'99, volume 1576 of Lecture Notes in Computer Science, pages 109-127. Springer-Verlag, 1999. [ bib | .ps.gz ]
[Bar99a] G. Barthe. Existence and uniqueness of normal forms in pure type systems with βη-conversion. In G. Gottlob, E. Grandjean, and K. Seyr, editors, Proceedings of CSL'98, volume 1584 of Lecture Notes in Computer Science, pages 241-259. Springer-Verlag, 1999. [ bib | .ps.gz ]
[Bar99d] G. Barthe. Type-Checking Injective Pure Type Systems. Journal of Functional Programming, 9(6):675-698, 1999. [ bib | .ps.gz ]
[Bar98a] G. Barthe. The relevance of proof-irrelevance. In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of ICALP'98, volume 1443 of Lecture Notes in Computer Science, pages 755-768. Springer-Verlag, 1998. [ bib | .ps.gz ]
[Bar98b] G. Barthe. The semi-full closure of Pure Type Systems. In L. Brim, J. Gruska, and J. Zlatuska, editors, Proceedings of MFCS'98, volume 1450 of Lecture Notes in Computer Science, pages 316-325. Springer-Verlag, 1998. [ bib | .ps.gz ]
[BHT98] G. Barthe, J. Hatcliff, and P. Thiemann. Monadic type systems: Pure type systems for impure settings. In A. Gordon, A. Pitts, and C. Talcott, editors, Proceedings of HOOTS'97, volume 10 of Electronic Notes in Theoretical Computer Science. Elsevier Publishing, 1998. [ bib | .ps.gz ]
[BR97] G. Barthe and F. van Raamsdonk. Termination of algebraic type systems: the syntactic approach. In M. Hanus and J. Heering, editors, Proceedings of ALP '97 - HOA '97, volume 1298 of Lecture Notes in Computer Science, pages 174-193. Springer-Verlag, 1997. [ bib | .ps.gz ]
[BKR97] G. Barthe, F. Kamareddine, and A. Ríos. Explicit substitutions for the λδ-calculus. In M. Hanus and J. Heering, editors, Proceedings of ALP '97 - HOA '97, volume 1298 of Lecture Notes in Computer Science, pages 209-223. Springer-Verlag, 1997. [ bib | .ps.gz ]
[BHS97a] G. Barthe, J. Hatcliff, and M.H. Sørensen. A notion of classical pure type system. In S. Brookes and M. Mislove, editors, Proceedings of MFPS'97, volume 6 of Electronic Notes in Theoretical Computer Science. Elsevier, 1997. [ bib | .ps.gz ]
[BHS97b] G. Barthe, J. Hatcliff, and M.H. Sørensen. Reflections on reflections. In H. Glaser, P. Hartel, and H. Kuchen, editors, Proceedings of PLILP'97, volume 1292 of Lecture Notes in Computer Science, pages 241-258, 1997. [ bib | .ps.gz ]
[BS97] G. Barthe and M.H. Sørensen. Domain-free pure type systems. In S. Adian and A. Nerode, editors, Proceedings of LFCS'97, volume 1234 of Lecture Notes in Computer Science, pages 9-20. Springer-Verlag, 1997. Superseded by journal version. [ bib ]
[BM97] G. Barthe and P.-A. Melliès. On the subject reduction property for algebraic type systems. In D. van Dalen and M. Bezem, editors, Proceedings of CSL'96, volume 1258 of Lecture Notes in Computer Science, pages 34-57. Springer-Verlag, 1997. [ bib | .ps.gz ]
[BE96] G. Barthe and H. Elbers. Towards lean proof checking. In J. Calmet and C. Limongelli, editors, Proceedings of DISCO'96, volume 1128 of Lecture Notes in Computer Science, pages 61-62. Springer-Verlag, 1996. Extended version. [ bib | .ps.gz ]
[BG96] G. Barthe and H. Geuvers. Modular properties of algebraic type systems. In G. Dowek, J. Heering, K. Meinke, and B. Möller, editors, HOA, volume 1074 of Lecture Notes in Computer Science, pages 37-56. Springer-Verlag, 1996. [ bib | .ps.gz ]
[BRB96] G. Barthe, M. Ruys, and H. Barendregt. A two-level approach towards lean proof-checking. In S. Berardi and M. Coppo, editors, Proceedings of TYPES'95, volume 1158 of Lecture Notes in Computer Science, pages 16-35. Springer-Verlag, 1996. [ bib | .ps.gz ]
[Bar96] G. Barthe. Implicit coercions in type systems. In S. Berardi and M. Coppo, editors, Proceedings of TYPES'95, volume 1158 of Lecture Notes in Computer Science, pages 1-15. Springer-Verlag, 1996. [ bib | .ps.gz ]
[BG95] G. Barthe and H. Geuvers. Congruence types. In H. Kleine Buening, editor, Proceedings of CSL'95, volume 1092 of Lecture Notes in Computer Science, pages 36-51. Springer-Verlag, 1995. [ bib | .ps.gz ]
[Bar95b] G. Barthe. A simple abstract semantics for equational theories. In H. Reichel, editor, Proceedings of FCT'95, volume 965 of Lecture Notes in Computer Science, pages 126-135. Springer-Verlag, 1995. [ bib | .ps.gz ]
[Bar95a] G. Barthe. Extensions of Pure Type Systems. In M. Dezani-Ciancaglini and G. Plotkin, editors, Proceedings of TLCA'95, volume 902 of Lecture Notes in Computer Science, pages 16-31. Springer-Verlag, 1995. [ bib | .ps.gz ]
[BPN0x] G. Barthe and L. Prensa-Nieto. Secure information flow for a concurrent language with scheduling. Journal of Computer Security, 200x. To appear. [ bib ]
[BCDdS0x] G. Barthe, P. Courtieu, G. Dufay, and S. Melo de Sousa. Jakarta: tool-assisted specification and verification of the JavaCard Platform. Journal of Automated Reasoning, 200x. To appear. [ bib ]
[BRB0x] G. Barthe, T. Rezk, and A. Basu. Security types preserving compilation. Journal of Computer Languages, Systems and Structures, 200x. To appear. [ bib | .pdf ]

This file has been generated by bibtex2html 1.87.

on Tue, 02 Sep 2008 00:00:08 +0200