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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
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 ]
G. Barthe and L. Prensa-Nieto.
Secure information flow for a concurrent language with scheduling.
Journal of Computer Security, 200x.
To appear.
[ bib ]