english version Toutes les publications de l'équipe
Publications - Gilles Barthe en format BibTeX
[Bibliographie en clair]

barthe.bib





@ARTICLE{ZanellaWMM07,
  author = {Gilles Barthe and Bejamin Gr{\'e}goire and 
	       Romain Janvier and Santiago Zanella B{\'e}guelin},
  title = {A Framework for Language-Based Cryptographic Proofs},
  booktitle = {2nd Informal ACM SIGPLAN Workshop on Mechanizing Metatheory},
  month = {Oct},
  year = {2007},
  topics = {team}
}
@INPROCEEDINGS{BBCGHLPR07:FMCO,
  author = {G. Barthe and L. Burdy and J. Charles and B. Gr{\'e}goire and M. Huisman and J.-L. Lanet and M. Pavlova and A. Requet},
  title = {{JACK}:  a tool for validation of security and behaviour of {Java} applications},
  booktitle = {FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  year = {2007},
  note = {To appear},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fmco06.pdf},
  topics = {team}
}
@ARTICLE{gl06:jcs,
  author = {G. Barthe and L. Prensa-Nieto},
  title = {Secure Information Flow for a Concurrent Language with
Scheduling},
  journal = {Journal of Computer Security},
  year = {200x},
  note = {To appear}
}
@INPROCEEDINGS{bgp:lpar06,
  author = {G. Barthe and B. Gr\'egoire and F. Pastawski},
  title = { Type-based termination of recursive definitions in the Calculus of Inductive Constructions},
  topics = {team},
  booktitle = {Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'06)},
  series = {Lecture Notes in Artificial Intelligence},
  year = 2006,
  month = {November},
  publisher = {Springer-Verlag},
  psurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/CICsombrero.ps.gz},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/CICsombrero.pdf.gz},
  note = {To appear}
}
@INPROCEEDINGS{Barthe:Gregoire:Kunz:Rezk:sas06,
  author = {G. Barthe and B. Gr{\'e}goire and C. Kunz 
            and T. Rezk},
  title = {Certificate Translation for Optimizing Compilers},
  booktitle = {Proceedings of the 13th International Static Analysis 
               Symposium (SAS)},
  year = {2006},
  publisher = {Springer-Verlag},
  series = {LNCS},
  address = {Seoul, Korea},
  month = {August},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Cesar.Kunz/publications/certtrans-SAS06.pdf},
  topics = {team}
}
@INPROCEEDINGS{Barthe:Kunz:esop08,
  author = {G. Barthe and C. Kunz},
  title = {Certificate Translation in Abstract Interpretation},
  booktitle = {Proceedings of the 17th European Symposium on Programming (ESOP)},
  year = {2008},
  publisher = {Springer-Verlag},
  series = {LNCS},
  address = {Budapest, Hungary},
  month = {March-April},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Cesar.Kunz/publications/ESOP08.pdf},
  topics = {team}
}
@INPROCEEDINGS{Barthe:Kunz:foal08,
  author = {G. Barthe and C. Kunz},
  title = {Certificate Translation for Specification-Preserving Advices},
  booktitle = {Proceedings of the Foundations of Aspect-Oriented Languages Workshop (FOAL)},
  year = {2008},
  publisher = {ACM},
  series = {},
  address = {Brussels, Belgium},
  month = {April},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Cesar.Kunz/publications/FOAL08.pdf},
  topics = {team}
}
@INPROCEEDINGS{gdt06:sp,
  author = {G. Barthe and D. Naumann and T. Rezk},
  title = { Deriving an Information Flow Checker and Certifying Compiler for {Java}},
  year = {2006},
  crossref = {sp06},
  psurl = {http://www-sop.inria.fr/everest/personnel/Tamara.Rezk//publication/Barthe-Naumann-Rezk.ps},
  topics = {team}
}
@MISC{gdt06:hal,
  author = {G. Barthe and D. Naumann and T. Rezk},
  title = {Deriving an Information Flow Checker and Certifying Compiler for {Java}},
  year = {2006},
  note = {To appear},
  topics = {team}
}
@TECHREPORT{gdt06:jvm,
  author = {G. Barthe and D. Pichardie and T. Rezk},
  title = {Deriving an Information Flow Checker for the {JVM}},
  year = {2006},
  topics = {team},
  institution = {INRIA}
}
@INPROCEEDINGS{gg05:fosad,
  author = {G. Barthe and G. Dufay},
  title = {{Formal methods for smartcard security}},
  pages = {133--177},
  crossref = {fosad05},
  pdfurl = {ftp://ftp-sop.inria.fr/lemme/personnel/Gilles.Barthe/fosad05.pdf},
  topics = {team}
}
@INPROCEEDINGS{BFPR06:flops,
  author = {G. Barthe and  J. Forest and  D. Pichardie and V. Rusu},
  title = {{Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant}},
  pages = {114-129},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/David.Pichardie/Publis/genfixpoint.pdf},
  psurl = {http://www-sop.inria.fr/everest/personnel/David.Pichardie/Publis/genfixpoint.ps.gz},
  topics = {team},
  crossref = {flops06}
}
@INPROCEEDINGS{gmg05:sefm,
  author = {G. Barthe and M. Pavlova and G. Schneider},
  title = {{Precise analysis of memory consumption using program logics}},
  crossref = {sefm05},
  pages = {86--95},
  pdfurl = {ftp://ftp-sop.inria.fr/lemme/personnel/Gilles.Barthe/sefm2005.pdf},
  topics = {team}
}
@INPROCEEDINGS{gta05:fast,
  author = {G. Barthe and T. Rezk and A. Saabas},
  title = {{Proof obligations preserving compilation}},
  year = {2005},
  crossref = {fast05},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Tamara.Rezk//publication/Barthe-Rezk-Saabas.pdf},
  pages = {112-126},
  topics = {team}
}
@INPROCEEDINGS{gs04:types,
  title = {A Machine-Checked Formalization of the Random Oracle Model},
  author = {G. Barthe and S. Tarento},
  crossref = {types04},
  topics = {team},
  pdfurl = {http://www-sop.inria.fr/everest/Sabrina.Tarento/Papers/ROM/main.pdf}
}
@INPROCEEDINGS{BGH02,
  author = {G. Barthe and D. Gurov and M. Huisman},
  title = {Compositional Verification of Secure Applet Interactions},
  crossref = {fase02},
  pages = {15-32},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/fase02.ps.gz},
  topics = {team}
}
@INPROCEEDINGS{BRW-qapl05,
  author = {G. Barthe and T. Rezk and M. Warnier},
  title = {Preventing Timing Leaks Through Transactional Branching Instructions},
  crossref = {qapl05},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Tamara.Rezk/publication/Barthe-Rezk-Warnier.pdf},
  topics = {team}
}
@INPROCEEDINGS{gbf05:tlca,
  author = {G. Barthe and B. Gr\'egoire and F. Pastawski},
  title = {Practical inference for typed-based termination in a polymorphic setting},
  crossref = {tlca05},
  pages = {71-85},
  topics = {team},
  psurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/Fsombrero.ps.gz}
}
@INPROCEEDINGS{gt05:tldi,
  author = {G. Barthe and T. Rezk},
  title = {Non-interference for a {JVM}-like language},
  crossref = {tldi05},
  pages = {103--112},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2005/BR05tldi.ps.gz}
}
@INPROCEEDINGS{gpt04:csfw,
  author = {G. Barthe and P. D'Argenio and T. Rezk},
  title = {{Secure Information Flow by Self-Composition}},
  crossref = {csfw04},
  pages = {100-114},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BDR04csfw.ps.gz}
}
@TECHREPORT{gpt06:hal,
  author = {G. Barthe and P. D'Argenio and T. Rezk},
  title = {{Secure Information Flow by Self-Composition}},
  topics = {team},
  year = {2006},
  institution = {INRIA}
}
@INPROCEEDINGS{gjs04:ijcar,
  author = {G. Barthe and J. Cederquist and S. Tarento},
  title = {{A Machine-Checked Formalization of the Generic Model
and the Random Oracle Model}},
  crossref = {ijcar04},
  pages = {385-399},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BCT04ijcar.ps.gz},
  topics = {team}
}
@INPROCEEDINGS{m+04:cardis,
  author = {M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet},
  title = {Enforcing High-Level Security Properties For Applets},
  crossref = {cardis04},
  pages = {},
  topics = {team},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/publis/P+04cardis.pdf}
}
@INPROCEEDINGS{gl04:fmse,
  author = {G. Barthe and L. Prensa-Nieto},
  title = {Formally Verifying Information Flow Type Systems for
Concurrent and Thread Systems},
  crossref = {fmse04},
  pages = {13-22},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BP04fmse.ps.gz}
}
@INPROCEEDINGS{gg04:fase,
  author = {G. Barthe and G. Dufay},
  title = {{A Tool-Assisted Framework for Certified Bytecode 
Verification}},
  pages = {99-113},
  crossref = {fase04},
  topics = {team,castles},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BD04fase.ps.gz}
}
@INPROCEEDINGS{gat04:vmcai,
  author = {G. Barthe and A. Basu and T. Rezk},
  title = {Security Types Preserving Compilation},
  crossref = {vmcai04},
  pages = {2--15},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/publis/2004/BBR04vmcai.ps.gz}
}
@INPROCEEDINGS{gs03:rta,
  author = {G. Barthe and S. Stratulat},
  title = {{Using Implicit Induction Techniques for the Validation of
the JavaCard Platform}},
  crossref = {rta03},
  pages = {337 - 351},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/rta03.ps.gz}
}
@INPROCEEDINGS{g+03:popl,
  author = {G. Barthe and H. Cirstea and C. Kirchner and L. Liquori},
  title = {Pure Pattern Type Systems},
  crossref = {popl03},
  topics = {team},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/popl03.ps.gz}
}
@INPROCEEDINGS{g+02:amast,
  author = {G. Barthe and P. Courtieu and G. Dufay and S. Melo
de Sousa},
  title = {{Tool-Assisted Specification and Verification
of the JavaCard Platform}},
  crossref = {amast02},
  pages = {41--59},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/amast02.ps.gz}
}
@INPROCEEDINGS{gt00:appsem,
  author = {G. Barthe and T. Coquand},
  title = {{An Introduction to Dependent Type Theory}},
  crossref = {appsem02},
  pages = {1--41},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/appsem00.ps.gz}
}
@INPROCEEDINGS{gp02:tphols,
  author = {G. Barthe and P. Courtieu},
  title = {{Efficient Reasoning about Executable Specifications in Coq}},
  crossref = {tphols02},
  pages = {31--46},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/tphols02.ps.gz}
}
@INPROCEEDINGS{g+02:vmcai,
  author = {G. Barthe and G. Dufay and L. Jakubiec and S. Melo
de Sousa},
  title = {{A formal correspondence between offensive and
defensive JavaCard virtual machines}},
  crossref = {vmcai02},
  pages = {32--45},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/vmcai02.ps.gz}
}
@INPROCEEDINGS{gt02:pepm,
  author = {G. Barthe and T. Uustalu},
  title = {CPS Translating Inductive and Coinductive Types},
  crossref = {pepm02},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/pepm02.ps.gz}
}
@INPROCEEDINGS{g+01:esmart,
  author = {G. Barthe and G. Dufay and M. Huisman and S. Melo de Sousa},
  title = {{Jakarta: a toolset to reason about the JavaCard platform}},
  crossref = {esmart01},
  pages = {2--18},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/esmart01.ps.gz}
}
@INPROCEEDINGS{go01:fossacs,
  author = {G. Barthe and O. Pons},
  title = {{Type Isomorphisms and Proof Reuse in Dependent Type Theory}},
  crossref = {fossacs01},
  pages = {57--71},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/fossacs01.ps.gz}
}
@INPROCEEDINGS{g+01:esop,
  author = {G. Barthe and G. Dufay and L. Jakubiec and
B. Serpette  and S. Melo de Sousa},
  title = {{A Formal Executable Semantics of the JavaCard Platform}},
  crossref = {esop01},
  pages = {302--319},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/esop01.ps.gz}
}
@INPROCEEDINGS{gb00:lpar,
  author = {G. Barthe and B. Serpette},
  title = {Static Reduction Analysis for Imperative Object Oriented Languages},
  crossref = {lpar00},
  pages = {344--361},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/lpar00.ps.gz}
}
@INPROCEEDINGS{gf00:fossacs,
  author = {Barthe, G. and Raamsdonk, F. van},
  title = {Constructor Subtyping in the Calculus of Inductive Constructions},
  crossref = {fossacs00},
  pages = {17--34},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/fossacs00.ps.gz}
}
@INPROCEEDINGS{gb99:flops,
  author = {G. Barthe and B. Serpette},
  title = {Partial evaluation and non-interference for object calculi},
  crossref = {flops99},
  pages = {53--67},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/flops99.ps.gz}
}
@INPROCEEDINGS{g99:fossacs,
  author = {G. Barthe},
  title = {Expanding the cube},
  crossref = {fossacs99},
  pages = {90--103},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/fossacs99.ps.gz}
}
@INPROCEEDINGS{gmj99:esop,
  author = {G. Barthe and M.J. Frade},
  title = {{Constructor subtyping}},
  crossref = {esop99},
  pages = {109--127},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/esop99.ps.gz}
}
@INPROCEEDINGS{g98:csl,
  author = {G. Barthe},
  title = {Existence and Uniqueness of Normal Forms in Pure Type Systems
with $\beta\eta$-conversion},
  crossref = {csl98},
  pages = {241--259},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/csl98.ps.gz}
}
@INPROCEEDINGS{g98:icalp,
  author = {G. Barthe},
  title = {The relevance of proof-irrelevance},
  crossref = {icalp98},
  pages = {755--768},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/icalp98.ps.gz}
}
@INPROCEEDINGS{g98:mfcs,
  author = {G. Barthe},
  title = {{The semi-full closure of Pure Type Systems}},
  crossref = {mfcs98},
  pages = {316--325},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/mfcs98.ps.gz}
}
@INPROCEEDINGS{gf97:hoa,
  author = {Barthe, G. and Raamsdonk, F. van},
  title = {Termination of Algebraic Type Systems:
the Syntactic Approach},
  crossref = {hoa97},
  pages = {174--193},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/hoa97.ps.gz}
}
@INPROCEEDINGS{gfa97:alp,
  author = {Barthe, G. and Kamareddine, F. and R{\'\i}os, A.},
  title = {Explicit substitutions for the $\lambda\Delta$-calculus},
  crossref = {alp97},
  pages = {209--223},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/alp97.ps.gz}
}
@INPROCEEDINGS{gjm97:mfps,
  author = {G. Barthe and J. Hatcliff and M.H. S{\o}rensen},
  title = {A notion of classical pure type system},
  crossref = {mfps97},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/mfps97.ps.gz}
}
@INPROCEEDINGS{gjm97:plilp,
  author = {G. Barthe and J. Hatcliff and M.H. S{\o}rensen},
  title = {Reflections on reflections},
  crossref = {plilp97},
  pages = {241--258},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/plilp97.ps.gz}
}
@INPROCEEDINGS{gm97:lfcs,
  author = {G. Barthe and M.H. S{\o}rensen},
  title = {Domain-free pure type systems},
  crossref = {lfcs97},
  pages = {9--20},
  note = {Superseded by journal version}
}
@INPROCEEDINGS{gpa96:csl,
  author = {G. Barthe and P.-A. Melli{\`e}s},
  title = {On the subject reduction property for algebraic type systems},
  crossref = {csl96},
  pages = {34--57},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/csl96.ps.gz}
}
@INPROCEEDINGS{gh96:disco,
  author = {G. Barthe and H. Elbers},
  title = {Towards lean proof checking},
  crossref = {disco96},
  pages = {61-62},
  note = {Extended version},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/disco96long.ps.gz}
}
@INPROCEEDINGS{gjp97:hoots,
  author = {G. Barthe and J. Hatcliff and P. Thiemann},
  title = {Monadic type systems: Pure Type Systems for Impure Settings},
  crossref = {hoots97},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/hoots97.ps.gz}
}
@INPROCEEDINGS{gh95:hoa,
  author = {G. Barthe and H. Geuvers},
  title = {Modular properties of algebraic type systems},
  crossref = {hoa95},
  pages = {37--56},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/hoa95.ps.gz}
}
@INPROCEEDINGS{gh95:csl,
  author = {G. Barthe and H. Geuvers},
  title = {Congruence types},
  crossref = {csl95},
  pages = {36-51},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/csl95.ps.gz}
}
@INPROCEEDINGS{gmh95:types,
  author = {G. Barthe and M. Ruys and H. Barendregt},
  title = {A two-level approach towards lean proof-checking},
  crossref = {types95},
  pages = {16--35},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/types95b.ps.gz}
}
@INPROCEEDINGS{g95:types,
  author = {G. Barthe},
  title = {Implicit coercions in type systems},
  crossref = {types95},
  pages = {1--15},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/types95.ps.gz}
}
@INPROCEEDINGS{g95:fct,
  author = {G. Barthe},
  title = {A simple abstract semantics for equational theories},
  crossref = {fct95},
  pages = {126--135},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/fct95.ps.gz}
}
@INPROCEEDINGS{g95:tlca,
  author = {G. Barthe},
  title = {{Extensions of Pure Type Systems}},
  crossref = {tlca95},
  pages = {16--31},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/tlca95.ps.gz}
}
@INPROCEEDINGS{BartheGH01,
  author = {G. Barthe and D. Gurov and M. Huisman},
  title = {Compositional specification and verification of control flow based security properties of multi-application programs},
  crossref = {ftfjp01},
  psurl = {ftp://ftp-sop.inria.fr/lemme/Marieke.Huisman/model_short.ps.gz}
}
@ARTICLE{g+:jakarta,
  author = {G. Barthe and P. Courtieu and G. Dufay  and S. Melo de 
Sousa},
  title = {{Jakarta: tool-assisted specification and verification of
the JavaCard Platform}},
  year = {200x},
  journal = {{Journal of Automated Reasoning}},
  note = {To appear},
  topics = {team,castles}
}
@ARTICLE{gat05:cl,
  author = {G. Barthe and  T. Rezk and A. Basu},
  title = {Security Types Preserving Compilation},
  year = {200x},
  journal = {Journal of Computer Languages, Systems and Structures},
  pdfurl = {http://www-sop.inria.fr/everest/Tamara.Rezk/publication/Barthe-Rezk-Basu.Journal.pdf},
  topics = {team},
  note = {To appear}
}
@ARTICLE{gt04:jfp,
  author = {G. Barthe and T. Coquand},
  title = {On the equational theory of non-normalizing Pure Type Systems},
  journal = {{Journal of Functional Programming}},
  year = {2004},
  volume = 14,
  number = 2,
  pages = {191--209},
  month = MAR,
  psurl = {ftp://ftp-sop.inria.fr/everest/Gilles.Barthe/fix.ps.gz},
  topics = {team}
}
@ARTICLE{gvo03:jfp,
  author = {G. Barthe and V. Capretta and O. Pons},
  title = {Setoids in Type Theory},
  journal = {{Journal of Functional Programming}},
  year = {2003},
  pages = {261--293},
  volume = 13,
  issue = 2,
  month = MAR
}
@ARTICLE{g+04:mscs,
  author = {G. Barthe and M. J. Frade  and E. Gim{\'e}nez and L. Pinto
and T. Uustalu},
  title = {Type-Based Termination of Recursive Definitions},
  year = {2004},
  journal = {{Mathematical Structures in Computer Science}},
  month = FEB,
  volume = 14,
  issue = 1,
  pages = {97--141},
  psurl = {ftp://ftp-sop.inria.fr/everest/Gilles.Barthe/tbt.ps.gz},
  topics = {team}
}
@ARTICLE{g04:mscs,
  author = {G. Barthe},
  title = {Type Isomorphisms and Back-and-Forth Coercions in Type 
Theory},
  year = {2005},
  journal = {{Mathematical Structures in Computer Science}},
  topics = {team}
}
@ARTICLE{gjm01:wnsn,
  author = {G. Barthe and J. Hatcliff and M.H. S{\o}rensen},
  title = {{Weak Normalization implies Strong Normalization in Generalized
Non-Dependent Pure Type Systems}},
  year = {2001},
  month = OCT,
  journal = {{Theoretical Computer Science}},
  pages = {317--361},
  volume = {269},
  number = {1-2}
}
@ARTICLE{gjm01:ip,
  author = {G. Barthe and J. Hatcliff and M.H.B. S{\o}rensen},
  title = {{An induction principle for Pure Type Systems}},
  year = {2001},
  month = SEP,
  journal = {{Theoretical Computer Science}},
  volume = {266},
  number = {1-2},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/tcs01.ps.gz},
  pages = {773-818}
}
@ARTICLE{gm00:jfp,
  author = {G. Barthe and M.H. S{\o}rensen},
  title = {{Domain-free pure type systems}},
  year = {2000},
  journal = {{Journal of Functional Programming}},
  month = SEP,
  pages = {417--452},
  volume = {10},
  number = {5},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/jfp00.ps.gz}
}
@ARTICLE{g99:jfp,
  author = {G. Barthe},
  title = {{Type-Checking Injective Pure Type Systems}},
  year = {1999},
  journal = {{Journal of Functional Programming}},
  volume = 9,
  number = 6,
  pages = {675--698},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/jfp99.ps.gz}
}
@ARTICLE{gjm99:hosc,
  author = {G. Barthe and J. Hatcliff and M.H. S{\o}rensen},
  title = {{CPS}-translations and applications: the cube and beyond},
  journal = {Higher-Order and Symbolic Computation},
  volume = 12,
  number = 2,
  year = 1999,
  month = SEP,
  pages = {125--170},
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/hosc99.ps.gz}
}
@ARTICLE{g99:ic,
  author = {G. Barthe},
  title = {Order-sorted inductive types},
  journal = {{Information and Computation}},
  pages = {42--76},
  month = FEB,
  year = 1999,
  volume = 149,
  number = 1,
  psurl = {ftp://ftp-sop.inria.fr/everest/personnel/Gilles.Barthe/ic99.ps.gz}
}
@PHDTHESIS{Bar:hdr,
  title = {De la th\'eorie des types \`a la v\'erification formelles 
des petits objets portables de s\'ecurit\'e},
  author = {G. Barthe},
  year = {2004},
  school = {Universit\'e de Nice Sophia-Antipolis},
  type = {Habilitation {\`a} Diriger des Recherches},
  topics = {team}
}
@TECHREPORT{mariela+03,
  author = {M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet},
  title = {Enforcing High-Level Security Properties For Applets},
  number = {RR-5061},
  institution = {INRIA},
  year = {2003},
  url = {http://www-sop.inria.fr/rapports/sophia/RR-5061.html},
  topics = {team}
}
@INPROCEEDINGS{BARTHE-EA-tgc06,
  author = {Gilles~Barthe
          and Lennart~Beringer
          and Pierre~Cr\'egut
          and Benjamin~Gr\'egoire
          and Martin~Hofmann
          and Peter~M{\"u}ller
          and Erik~Poll
          and Germ\'{a}n~Puebla
          and Ian~Stark
          and Eric~V\'etillard},
  title = {MOBIUS: Mobility, Ubiquity, Security. Objectives and progress
         report},
  booktitle = {TGC 2006: Proceedings of the second symposium on Trustworthy 
            Global Computing},
  series = {LNCS},
  publisher = {Springer-Verlag},
  year = {2006},
  topics = {team},
  url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/tgc06.pdf}
}
@PROCEEDINGS{flops06,
  booktitle = {Proceedings of FLOPS'06},
  title = {Proceedings of FLOPS'06},
  year = 2006,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = 3945,
  editor = {M. Hagiya and P. Wadler}
}
@PROCEEDINGS{sp06,
  booktitle = {Proceedings of Symposium of Security and Privacy'06},
  title = {Proceedings of Proceedings of Symposium of Security and Privacy '06},
  year = 2006,
  publisher = {IEEE Press},
  editor = {}
}
@PROCEEDINGS{sefm05,
  title = {Software Engineering and Formal Methods (SEFM'05)},
  booktitle = {Proceedings of SEFM'05},
  editor = {B. Aichernig and B. Beckert},
  publisher = {IEEE Computer Society},
  month = {September},
  address = {Koblenz, Germany},
  year = 2005
}
@PROCEEDINGS{fosad05,
  year = {2005},
  booktitle = {Proceedings of FOSAD'05},
  editor = {A.~Aldini and R.~Gorrieri and F.~Martinelli},
  series = {Lecture Notes in Computer Science},
  volume = {3655},
  publisher = {Springer-Verlag}
}
@PROCEEDINGS{fast05,
  booktitle = {Proceedings of FAST'05},
  year = 2005,
  editor = {R.~Gorrieri and F.~Martinelli and P.~Ryan and S.~Schneider},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  volume = {3866}
}
@PROCEEDINGS{qapl05,
  title = {Proceedings of 3rd Workshop on Quantitative Aspects of 
Programming Languages (QAPL'05)},
  booktitle = {Proceedings of 3rd Workshop on Quantitative Aspects of 
Programming Languages (QAPL'05)},
  year = {2005},
  address = {Edinburgh, Scotland },
  publisher = {Electronic Notes in Theoretical Computer Science},
  note = {to appear}
}
@PROCEEDINGS{tlca05,
  title = {Proceedings of {TLCA}'05},
  booktitle = {Proceedings of {TLCA}'05},
  year = {2005},
  editor = {P. Urzyczyn},
  volume = 3641,
  series = {Lecture Notes in Computer Science},
  address = {Nara, Japan},
  month = {April},
  publisher = {Springer-Verlag}
}
@PROCEEDINGS{tldi05,
  title = {Proceedings of {TLDI}'05},
  booktitle = {Proceedings of {TLDI}'05},
  year = {2005},
  editor = {M. F\"ahndrich},
  publisher = {ACM Press},
  month = {January},
  address = {Long Beach, USA}
}
@PROCEEDINGS{types04,
  year = {2005},
  editor = {J.C. Filli\^atre and C. Paulin-Mohring and B. Werner},
  booktitle = {Proceedings of {TYPES}'04},
  title = {Proceedings of {TYPES}'04},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  volume = {3839}
}
@PROCEEDINGS{csfw04,
  title = {Proceedings of CSFW'04},
  booktitle = {Proceedings of CSFW'04},
  year = {2004},
  editor = {R. Foccardi},
  publisher = {IEEE Press},
  address = {Pacific Grove,USA},
  month = {June}
}
@PROCEEDINGS{ijcar04,
  year = {2004},
  title = {Proceedings of IJCAR'04},
  booktitle = {Proceedings of IJCAR'04},
  editor = {D. Basin and M. Rusinowitch},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  volume = {3097},
  address = {Cork, Ireland},
  month = {July}
}
@PROCEEDINGS{cardis04,
  editor = {P. Paradinas and J.-J. Quisquater},
  booktitle = {{Proceedings of CARDIS'04}},
  title = {{Proceedings of CARDIS'04}},
  publisher = {Kluwer Academic Publishers},
  year = {2004},
  address = {Toulouse, France},
  month = {August}
}
@PROCEEDINGS{fmse04,
  booktitle = {Proceedings of FMSE'04},
  title = {Proceedings of FMSE'04},
  editor = {M. Backes and D. Basin and M. Waidner},
  publisher = {ACM Press},
  year = 2004,
  address = {Washington D.C., USA},
  month = {October}
}
@PROCEEDINGS{fase04,
  year = {2004},
  booktitle = {Proceedings of {FASE}'04},
  title = {Proceedings of {FASE}'04},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  volume = {2984},
  editor = {M. Wermelinger and T. Margaria-Steffen},
  address = {Barcelona, Spain},
  month = {March}
}
@PROCEEDINGS{vmcai04,
  year = {2004},
  booktitle = {Proceedings of {VMCAI}'04},
  title = {Proceedings of {VMCAI}'04},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  volume = {2934},
  editor = {B. Steffen and G. Levi},
  address = {Venice, Italy},
  month = {January}
}
@PROCEEDINGS{rta03,
  year = {2003},
  booktitle = {Proceedings of RTA'03},
  title = {Proceedings of RTA'03},
  editor = {R. Nieuwenhuis},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  volume = {2706},
  address = {Valencia, Spain},
  month = {June}
}
@PROCEEDINGS{popl03,
  booktitle = {Proceedings of POPL'03},
  title = {Proceedings of POPL'03},
  year = {2003},
  publisher = {ACM Press},
  address = {New Orleans, USA},
  month = {January}
}
@PROCEEDINGS{fase02,
  booktitle = {Fundamental Approaches to Software Engineering (FASE'02)},
  title = {Fundamental Approaches to Software Engineering (FASE'02)},
  year = {2002},
  series = {Lecture Notes in Computer Science},
  volume = {2306},
  publisher = {Springer-Verlag}
}
@PROCEEDINGS{amast02,
  booktitle = {Proceedings of AMAST'02},
  title = {Proceedings of AMAST'02},
  editor = {H. Kirchner and C. Ringessein},
  series = {Lecture Notes in Computer Science},
  year = {2002},
  publisher = {Springer-Verlag},
  volume = {2422}
}
@PROCEEDINGS{appsem02,
  booktitle = {Applied Semantics. Lecture Notes for the APPSEM Summer 
School},
  title = {Applied Semantics. Lecture Notes for the APPSEM Summer School},
  year = {2002},
  editor = {G. Barthe and P. Dybjer and L. Pinto and J. Saraiva},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  volume = {2395}
}
@PROCEEDINGS{pepm02,
  editor = {P. Thiemann},
  booktitle = {Proceedings of PEPM'02},
  title = {Proceedings of PEPM'02},
  publisher = {ACM Press},
  year = {2002}
}
@PROCEEDINGS{tphols02,
  booktitle = {Proceedings of TPHOLs'02},
  title = {Proceedings of TPHOLs'02},
  editor = {V. Carre{\~n}o and C. Mu{\~n}oz and S. Tahar},
  series = {Lecture Notes in Computer Science},
  year = {2002},
  publisher = {Springer-Verlag},
  volume = {2410}
}
@PROCEEDINGS{vmcai02,
  year = {2002},
  booktitle = {Proceedings of VMCAI'02},
  title = {Proceedings of VMCAI'02},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {2294},
  editor = {A. Cortesi}
}
@PROCEEDINGS{ftfjp01,
  title = {Workshop on Formal Techniques for Java Programs (FTfJP)},
  booktitle = {Workshop on Formal Techniques for Java Programs (FTfJP)},
  year = 2001,
  url = {http://www.informatik.fernuni-hagen.de/import/pi5/workshops/ecoop2001_papers.html}
}
@PROCEEDINGS{esmart01,
  year = {2001},
  booktitle = {Proceedings of e-SMART'01},
  title = {Proceedings of e-SMART'01},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {2140},
  editor = {I. Attali and T. Jensen}
}
@PROCEEDINGS{fossacs01,
  year = {2001},
  booktitle = {Proceedings of {FOSSACS}'01},
  title = {Proceedings of {FOSSACS}'01},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {2030},
  editor = {F. Honsell and M. Miculan}
}
@PROCEEDINGS{esop01,
  year = {2001},
  booktitle = {Proceedings of ESOP'01},
  title = {Proceedings of ESOP'01},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {2028},
  editor = {D. Sands}
}
@PROCEEDINGS{lpar00,
  booktitle = {Proceedings of LPAR'00},
  title = {Proceedings of LPAR'00},
  year = 2000,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1955},
  editor = {M. Parigot and A. Voronkov}
}
@PROCEEDINGS{fossacs00,
  booktitle = {Proceedings of {FOSSACS}'00},
  title = {Proceedings of {FOSSACS}'00},
  year = 2000,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1784},
  editor = {J. Tuyrin}
}
@PROCEEDINGS{flops99,
  booktitle = {Proceedings of FLOPS'99},
  title = {Proceedings of FLOPS'99},
  year = 1999,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1722},
  editor = {A. Middeldorp and T. Sato}
}
@PROCEEDINGS{fossacs99,
  booktitle = {Proceedings of {FOSSACS}'99},
  title = {Proceedings of {FOSSACS}'99},
  year = 1999,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1578},
  editor = {W. Thomas}
}
@PROCEEDINGS{esop99,
  year = {1999},
  booktitle = {Proceedings of {ESOP}'99},
  title = {Proceedings of {ESOP}'99},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1576},
  editor = {D. Swiestra}
}
@PROCEEDINGS{csl98,
  year = {1999},
  booktitle = {Proceedings of CSL'98},
  title = {Proceedings of CSL'98},
  editor = {G. Gottlob and E. Grandjean and K. Seyr},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1584}
}
@PROCEEDINGS{icalp98,
  booktitle = {Proceedings of ICALP'98},
  title = {Proceedings of ICALP'98},
  year = 1998,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1443},
  editor = {K.G. Larsen and S. Skyum and G. Winskel}
}
@PROCEEDINGS{mfcs98,
  booktitle = {Proceedings of MFCS'98},
  title = {Proceedings of MFCS'98},
  year = 1998,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1450},
  editor = {L. Brim and J. Gruska and J. Zlatuska}
}
@PROCEEDINGS{hoa97,
  booktitle = {Proceedings of ALP '97 - HOA '97},
  title = {Proceedings of ALP '97 - HOA '97},
  year = 1997,
  editor = {Hanus, M. and Heering, J.},
  volume = 1298,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag}
}
@PROCEEDINGS{alp97,
  booktitle = {Proceedings of ALP '97 - HOA '97},
  title = {Proceedings of ALP '97 - HOA '97},
  year = 1997,
  editor = {Hanus, M. and Heering, J.},
  volume = 1298,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag}
}
@PROCEEDINGS{mfps97,
  year = {1997},
  series = {Electronic Notes in Theoretical Computer Science},
  editor = {S. Brookes and M. Mislove},
  volume = {6},
  booktitle = {Proceedings of MFPS'97},
  title = {Proceedings of MFPS'97},
  publisher = {Elsevier}
}
@PROCEEDINGS{plilp97,
  booktitle = {Proceedings of PLILP'97},
  title = {Proceedings of PLILP'97},
  editor = {H. Glaser and P. Hartel and H. Kuchen},
  series = {Lecture Notes in Computer Science},
  volume = 1292,
  year = {1997}
}
@PROCEEDINGS{lfcs97,
  year = {1997},
  booktitle = {Proceedings of LFCS'97},
  title = {Proceedings of LFCS'97},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  editor = {S. Adian and A. Nerode},
  volume = {1234}
}
@PROCEEDINGS{hoots97,
  year = {1998},
  booktitle = {Proceedings of HOOTS'97},
  title = {Proceedings of HOOTS'97},
  editor = {A. Gordon and A. Pitts and C. Talcott},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = 10,
  publisher = {Elsevier Publishing}
}
@PROCEEDINGS{csl96,
  booktitle = {Proceedings of CSL'96},
  title = {Proceedings of CSL'96},
  series = {Lecture Notes in Computer Science},
  editor = {D. van Dalen and M. Bezem},
  publisher = {Springer-Verlag},
  year = {1997},
  volume = {1258}
}
@PROCEEDINGS{disco96,
  year = {1996},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  booktitle = {Proceedings of DISCO'96},
  title = {Proceedings of DISCO'96},
  editor = {J. Calmet and C. Limongelli},
  volume = {1128}
}
@PROCEEDINGS{hoa95,
  editor = {G. Dowek and
               J. Heering and
               K. Meinke and
               B. M{\"o}ller},
  title = {Proceeding of  HOA'95},
  booktitle = {HOA},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1074},
  year = {1996}
}
@PROCEEDINGS{types95,
  year = {1996},
  booktitle = {Proceedings of {TYPES}'95},
  title = {Proceedings of {TYPES}'95},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  editor = {S. Berardi and M. Coppo},
  volume = {1158}
}
@PROCEEDINGS{fct95,
  year = {1995},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {965},
  editor = {H. Reichel},
  booktitle = {Proceedings of FCT'95},
  title = {Proceedings of FCT'95}
}
@PROCEEDINGS{tlca95,
  booktitle = {{Proceedings of TLCA'95}},
  title = {{Proceedings of TLCA'95}},
  year = 1995,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {902},
  editor = {M. Dezani-Ciancaglini and G. Plotkin}
}
@PROCEEDINGS{csl95,
  booktitle = {{Proceedings of CSL'95}},
  title = {{Proceedings of CSL'95}},
  year = 1995,
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1092},
  editor = {H. Kleine Buening}
}

This file has been generated by bibtex2html 1.87.

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