version française All team publications
Publications - Benjamin Gregoire
[BibTeX Format]

[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 ]
[BBC+07] G. Barthe, L. Burdy, J. Charles, B. Grégoire, M. Huisman, J.-L. Lanet, M. Pavlova, and A. Requet. JACK: a tool for validation of security and behaviour of Java applications. In FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects, Lecture Notes in Computer Science. Springer-Verlag, 2007. To appear. [ bib | .pdf ]
[BGP06] 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 ]
[BGKR06] 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 ]
[GTW06] 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 ]
[GT06] 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 ]
[BBC+06] 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 ]
[GM05] B. Grégoire and A. Mahboubi. Proving equalities in a commutative ring done right in Coq. In J. Hurd and T. Melham, editors, Proceedings of TPHOLs'05, volume 3603 of Lecture Notes in Computer Science, pages 98-113, Oxford, UK, August 2005. Springer-Verlag. [ bib | .ps.gz ]
[BG05] B. Barras and B. Grégoire. On the role of type decorations in the calculus of inductive constructions. In L. Ong, editor, Proceedings of CSL'05, volume 3634 of Lecture Notes in Computer Science, pages 151-166, Oxford, UK, August 2005. Springer-Verlag. [ bib | .ps.gz ]
[BGP05] 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 ]
[BGL05] Y. Bertot, B. Grégoire, and X. Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In J.C. Filliâtre, C. Paulin-Mohring, and B. Werner, editors, Proceedings of TYPES'04, volume 3839 of Lecture Notes in Computer Science, pages 66 - 81. Springer-Verlag, 2005. [ bib | .ps.gz ]
[Gré03] B. Grégoire. Compilation des termes de preuves: un (nouveau) mariage entre Coq et Ocaml. Thése de doctorat, spécialité informatique, Université Paris 7, école Polytechnique, France, December 2003. [ bib | .ps.gz ]
[GL02] B. Grégoire and X. Leroy. A compiled implementation of strong reduction. In International Conference on Functional Programming 2002, pages 235-246. ACM Press, 2002. [ bib | .pdf ]

This file has been generated by bibtex2html 1.87.

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