@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}
}
@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}
}
@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}
}
@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}
}
@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{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{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{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}
}
@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}
}
@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{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{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}
}