Journal papers
[Format BibTeX ]
[GS07 ]
Benjamin Grégoire and Jorge Luis Sacchini.
Combining a verification condition generator for a bytecode language
with static analyses.
2007.
To appear.
[ bib ]
[BGJB07 ]
Gilles Barthe , Bejamin Grégoire , Romain Janvier, and Santiago Zanella
Béguelin.
A framework for language-based cryptographic proofs.
Oct 2007.
[ bib ]
[Bar05 ]
G. Barthe .
Type isomorphisms and back-and-forth coercions in type theory.
Mathematical Structures in Computer Science , 2005.
[ bib ]
[BCHJ05 ]
C. Breunesse, N. Cataño , M. Huisman , and B. Jacobs.
Formal methods for smart cards: an experience report.
Science of Computer Programming , 55(1-3):53-80, 2005.
[ bib |
.pdf ]
[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 ]
[BCR03 ]
L. Burdy , L. Casset, and A. Requet.
Développement d'un vérifieur de byte-code embarqué.
Technique et Science Informatiques , 22(1):33-60, 2003.
[ bib |
.ps.gz ]
[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:10 +0200