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 ]
M. Huisman, P. Worah, and K. Sunesen.
A temporal logic characterisation of observational determinism.
In 19th IEEE Computer Security Foundations Workshop. IEEE
Computer Society, July 2006.
[ bib |
.pdf ]
J. Charles.
Adding native specifications to JML.
In Proceedings of the ECOOP workshop on Formal Techniques for
Java-like Programs (FTfJP'2006), 2006.
[ bib |
.ps ]
Santiago Zanella Béguelin, Gustavo Betarte, and Carlos Luna.
A formal specification of the MIDP 2.0 security model.
In Theodosis Dimitrakos, Fabio Martinelli, Peter Y. A. Ryan, and
Steve A. Schneider, editors, Formal Aspects in Security and Trust,
Fourth International Workshop, FAST 2006, Hamilton, Ontario, Canada, August
26-27, 2006, Revised Selected Papers, volume 4691 of Lecture Notes in
Computer Science, pages 220-234. Springer-Verlag, 2006.
[ bib |
.pdf |
http ]
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 ]
B. Grégoire, L. Thery, and B. Werner.
A computational approach to Pocklington certificates in type
theory.
In M. Hagiya and P. Wadler, editors, Proceedings of FLOPS'06,
volume 3945 of Lecture Notes in Computer Science, pages 97 - 113.
Springer-Verlag, 2006.
[ bib |
.pdf ]
B. Grégoire and L. Thery.
A purely functional library for modular arithmetic and its
application for certifying large prime numbers.
In U. Furbach and N. Shankar, editors, Proceedings of IJCAR'06,
volume 4130 of Lecture Notes in Artificial Intelligence, pages
423-437. Springer-Verlag, 2006.
[ bib |
.pdf ]
S. Tarento.
Formalisation en Coq de modeles cryptographiques et application
au cryptosysteme ElGamal.
PhD thesis, Université de Nice Sophia-Antipolis, 2006.
[ bib ]
A. Courbot, M. Pavlova, G. Grimaud, and J.J. Vandewalle.
A low-footprint Java-to-native compilation scheme using formal
methods.
In J. Domingo-Ferrer, J. Posegga, and D. Schreckling, editors,
proceedings of CARDIS, volume 3928 of Lecture Notes in Computer
Science, pages 329-344. Springer, 2006.
[ bib ]
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 ]