english version Toutes les publications de l'équipe
Publications - Benjamin Gregoire en format BibTeX
[Bibliographie en clair]

gregoire.bib





@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{BBCGHLPR07:FMCO,
  author = {G. Barthe and L. Burdy and J. Charles and B. Gr{\'e}goire and M. Huisman and J.-L. Lanet and M. Pavlova and A. Requet},
  title = {{JACK}:  a tool for validation of security and behaviour of {Java} applications},
  booktitle = {FMCO: Proceedings of 5th International Symposium on Formal Methods for Components and Objects},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  year = {2007},
  note = {To appear},
  pdfurl = {ftp://ftp-sop.inria.fr/everest/Marieke.Huisman/fmco06.pdf},
  topics = {team}
}
@INPROCEEDINGS{bgp:lpar06,
  author = {G. Barthe and B. Gr\'egoire and F. Pastawski},
  title = { Type-based termination of recursive definitions in the Calculus of Inductive Constructions},
  topics = {team},
  booktitle = {Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'06)},
  series = {Lecture Notes in Artificial Intelligence},
  year = 2006,
  month = {November},
  publisher = {Springer-Verlag},
  psurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/CICsombrero.ps.gz},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/CICsombrero.pdf.gz},
  note = {To appear}
}
@INPROCEEDINGS{Barthe:Gregoire:Kunz:Rezk:sas06,
  author = {G. Barthe and B. Gr{\'e}goire and C. Kunz 
            and T. Rezk},
  title = {Certificate Translation for Optimizing Compilers},
  booktitle = {Proceedings of the 13th International Static Analysis 
               Symposium (SAS)},
  year = {2006},
  publisher = {Springer-Verlag},
  series = {LNCS},
  address = {Seoul, Korea},
  month = {August},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Cesar.Kunz/publications/certtrans-SAS06.pdf},
  topics = {team}
}
@INPROCEEDINGS{GTW:flops,
  author = {B. Gr\'egoire and L. Thery and B. Werner},
  title = {A computational approach to {Pocklington} certificates in type 
theory},
  topics = {team},
  pages = {97 - 113},
  pdfurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/pock.pdf},
  crossref = {flops06}
}
@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{gbf05:tlca,
  author = {G. Barthe and B. Gr\'egoire and F. Pastawski},
  title = {Practical inference for typed-based termination in a polymorphic setting},
  crossref = {tlca05},
  pages = {71-85},
  topics = {team},
  psurl = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/Fsombrero.ps.gz}
}
@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.}
}
@INPROCEEDINGS{Bertot-Gregoire-Leroy-04,
  author = {Y. Bertot and B. Gr{\'e}goire and X. Leroy},
  title = {A structured approach to proving compiler optimizations based on dataflow analysis},
  url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/concert.ps.gz},
  pages = {66 - 81},
  topics = {team},
  crossref = {types04}
}
@INPROCEEDINGS{Gregoire-Mahboubi-05,
  author = {B. Gr{\'e}goire and A. Mahboubi},
  title = {Proving equalities in a commutative ring done right in {Coq}},
  crossref = {tphol05},
  url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/newring.ps.gz},
  pages = {98--113},
  topics = {team}
}
@INPROCEEDINGS{Gregoire-Barras-05,
  author = {B. Barras and B. Gr{\'e}goire},
  title = {On the role of type decorations in the Calculus of Inductive Constructions},
  topics = {team},
  url = {http://www-sop.inria.fr/everest/personnel/Benjamin.Gregoire/Publi/equiv.ps.gz},
  pages = {151-166},
  crossref = {csl05}
}
@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
}

This file has been generated by bibtex2html 1.87.

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