@ARTICLE{GregoireS07,
author = {Benjamin Gr{\'e}goire and Jorge Luis Sacchini},
title = {Combining a Verification Condition Generator for a Bytecode
Language with Static Analyses},
year = {2007},
note = {To appear},
topics = {team}
}
@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}
}
@INPROCEEDINGS{GT:ijcar06,
author = {B. Gr\'egoire and L. Thery},
title = {A purely functional library for modular arithmetic and its application for certifying large prime numbers},
topics = {team},
pages = {423-437},
booktitle = {Proceedings of IJCAR'06},
year = 2006,
publisher = {Springer-Verlag},
series = {Lecture Notes in Artificial Intelligence},
volume = 4130,
editor = {U. Furbach and N. Shankar},
pdfurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/numlib.pdf}
}
@INPROCEEDINGS{Gregoire-Leroy-02,
author = {B. Gr{\'e}goire and X. Leroy},
title = {A compiled implementation of strong reduction},
pages = {235--246},
crossref = {icfp02},
url = {http://pauillac.inria.fr/~xleroy/publi/strong-reduction.pdf},
abstract = {Motivated by applications to proof assistants based on dependent
types, we develop and prove correct a strong reducer and
$\beta$-equivalence checker for the $\lambda$-calculus with products,
sums, and guarded fixpoints. Our approach is based on compilation to
the bytecode of an abstract machine performing weak reductions on
non-closed terms, derived with minimal modifications from the ZAM
machine used in the Objective Caml bytecode interpreter, and
complemented by a recursive ``read back'' procedure. An
implementation in the Coq proof assistant demonstrates important
speed-ups compared with the original interpreter-based implementation
of strong reduction in Coq.}
}
@PHDTHESIS{GregoirePhd,
author = {B. Gr{\'e}goire},
title = {Compilation des termes de preuves: un (nouveau) mariage entre Coq et Ocaml.},
school = {Universit\'e Paris 7},
year = {2003},
type = {Th\'ese de doctorat, sp\'ecialit\'e informatique},
address = {\'ecole Polytechnique, France},
month = {December},
url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/gregoire_these.ps.gz}
}
@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{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{csl05,
title = {Proceedings of CSL'05},
booktitle = {Proceedings of CSL'05},
year = {2005},
address = {Oxford, UK},
month = {August},
volume = {3634},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
editor = {L. Ong}
}
@PROCEEDINGS{tphol05,
title = {Proceedings of TPHOLs'05},
booktitle = {Proceedings of TPHOLs'05},
editor = {J. Hurd and T. Melham},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
volume = 3603,
year = {2005},
address = {Oxford, UK},
month = {August}
}
@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{icfp02,
booktitle = {International Conference on Functional Programming 2002},
title = {International Conference on Functional Programming 2002},
publisher = {ACM Press},
year = 2002
}