@string{jfp ="Journal of Functional Programming"}
@string{mscs ="Mathematical structures in Computer Science"}
@string{acmcs = "ACM Computing Surveys"}
@string{acta = "Acta Informatica"}
@string{amast02         = "Algebraic Methodology And Software
                  Technology (AMAST~'02)"}
@string{cacm = "Communications of the ACM"}
@string{CJ = "Computer Journal"}
@string{fme02           = "Formal Methods Europe (FME~'02)"}
@string{ibmjrd = "IBM Journal of Research and Development"}
@string{ibmsj = "IBM Systems Journal"}
@string{ieeese = "IEEE Transactions on Software Engineering"}
@string{ieeetc = "IEEE Transactions on Computers"}
@string{INRIA = "Institut National de Recherche en Informatique et en Automatique"}
@string{ipl = "Information Processing Letters"}
@string{JACM = "Journal of the Association for Computing Machinery"}
@string{jcss = "Journal of Computer and System Sciences"}
@string{JSC = "Journal of Symbolic Computation"}
@string{Jaaecc = "J.~Applied Algebra to Engineering and Code-Correcting"}
@string{scp = "Science of Computer Programming"}
@string{sicomp = "SIAM Journal on Computing"}
@string{siamNA = "SIAM Journal on Numerical Analysis"}
@string{ISSAC = "Proc.\ ACM Intern. Symp. on Symbolic and Algebraic Computation"}
@string{AAECC = "Proc.\ Intern.\ Symp.\ Applied Algebra, Algebraic Algorithms
        and Error-Correcting Codes"}
@string{stoc = "Proc.\ ACM Symp.\ Theory of Computing"}
@string{focs="Proc.\ IEEE Symp.\ Foundations of Comp.\ Sci."}
@string{springer="Springer-Verlag"}
@string{lncs="Lecture Notes in Computer Science"}
@string{sigsam = "SIGSAM Bulletin"}
@string{tocs = "ACM Transactions on Computer Systems"}
@string{tods = "ACM Transactions on Database Systems"}
@string{tog = "ACM Transactions on Graphics"}
@string{toms = "ACM Transactions on Mathematical Software"}
@string{toplas = "ACM Transactions on Programming Languages and Systems"}
@string{tcs = "Theoretical Computer Science"}
@string{LNCS = "Lecture Notes in Computer Science"}
@string{UNSA = "Universit\'e de Nice-Sophia Antipolis"}
@string{focs="Proc.\ IEEE Symp.\ Foundations of Comp.\ Sci."}
@string{cccg="Proc.\ Canadian Conf.\ on Computational Geometry"}
@string{stoc = "Proc.\ ACM Symp.\ Theory of Comp."}
@string{scog ="Proc.\ ACM Symp.\ on Computational Geometry"}
@string{dcgeometry="Discr.~and Comput.~Geometry"}
@string{CRAS="Comptes rendus de l'Acad\'emie des Sciences de Paris"}


@INPROCEEDINGS{lchicli01a,
        title           = "Une formalisation des faisceaux et des schémas affines en théorie des types avec Coq",
        author          = "Laurent Chicli",
   booktitle =    "Journées Francophones des Langages Applicatifs",
        publisher =    "INRIA",
        address =      "Pontarlier, France",
        year =         "2001",
note={Also appears as INRIA Research Report 4216}}


@INPROCEEDINGS{LPjfla01,
        title           = "Extraction dans le CCI",
        author          = "Loïc Pottier",
   booktitle =    "Journées Francophones des Langages Applicatifs",
        publisher =    "INRIA",
        address =      "Pontarlier, France",
        year =         "2001",
note={Also appears as INRIA Research Report 4026, October 2000.}}



@inproceedings{assialoic01,
  author = {Assia Mahboubi and Loïc Pottier},
  title = {Elimination des quantificateurs sur les réels en Coq},
  year = {2002},
  booktitle={Proceedings of JFLA'02},
  editor={L. Rideau}
}

@INPROCEEDINGS{lt::float,
        title           = "{A} {G}eneric {L}ibrary for {F}loating-{P}oint {N}umbers and its {A}pplication to {E}xact {C}omputing",
        author          = "Marc Daumas and Laurence Rideau and Laurent Th{\'e}ry",
   booktitle =    "Theorem Proving in Higher Order Logics: 14th
                  International Conference, TPHOLs'01",
        publisher =    "Springer-Verlag",
        address =      "Edimbourg, {\'E}cosse",
        month=sep,
        year =         "2001",
        series =       "LNCS",
        number=2152
}



@INPROCEEDINGS{PichardieBertot01,
        title           = "Formalizing Convex Hull Algorithms",
        author          = "David Pichardie and Yves Bertot",
   booktitle =    "Theorem Proving in Higher Order Logics: 14th
                  International Conference, TPHOLs'01",
        publisher =    "Springer-Verlag",
        address =      "Edimbourg, {\'E}cosse",
        month=sep,
        year =         "2001",
        series =       "LNCS",
        number=2152
}

@INPROCEEDINGS{BertotCAV01,
        title           = "Formalizing a JVML verifier for initialization in a theorem prover",
        author          = "Yves Bertot",
   booktitle =    "Computer Aided Verification (CAV'01)",
        publisher =    "Springer-Verlag",
        address =      "Paris, France",
        month=jul,
        year =         "2001",
        series =       "LNCS",
        number=2102,
note={Full version appears as INRIA Technical Report, November 2000.}}



@inproceedings{lc00b,
   author = {Laurent Chicli},
   title = {Formalizing Sheaves and Schemes in Coq},
   BOOKTITLE = {Workshop Types, Durham, Angleterre},
   month = {Décembre},
   year = {2000}
}


@inproceedings{Bertot99a,
   author = {Yves Bertot},
   title = {Ctcoq et PCoq},
   BOOKTITLE = {Poster presented at ISSAC'99, Vancouver, Canada},
   month = {juillet},
   year = {1999}
}


@inproceedings{Bertot99b,
   author = {Yves Bertot},
   title = {Ctcoq et PCoq},
   BOOKTITLE = {FM'99, Toulouse, colloque satellite des utilisateurs de Coq},
   month = {septembre},
   year = {1999}
}

@inproceedings{Pottier99a,
   author = {Loïc Pottier},
   title = {La contrib algebra de Coq},
   BOOKTITLE = {FM'99, Toulouse, colloque satellite des utilisateurs de Coq},
   month = {septembre},
   year = {1999}
}

@inproceedings{Pottier99b,
   author = {Loïc Pottier},
   title = {Formalization of algebra in Coq and Ctcoq},
   BOOKTITLE = {Workshop Types, Lökeberg, Suède},
   month = {juin},
   year = {1999}
}

@inproceedings{LP2000c,
   author = {Loïc Pottier},
   title = {Extraction in Coq},
   BOOKTITLE = {Workshop Types, Durham, Angleterre},
   month = {Decembre},
   year = {2000}
}

@INPROCEEDINGS{LPtphol01,
        title           = "Quotients in the CIC",
        author          = "Loïc Pottier",
   booktitle =    "Supplementary Proceedings of 
           Theorem Proving in Higher Order Logics: 14th
                  International Conference, TPHOLs'01",
        publisher =    "University of Edinburgh",
        address =      "Edimbourg, {\'E}cosse",
        month=sep,
        year =         "2001",
note={Also appears as INRIA Research Report, November 2000.}}



@TECHREPORT{lt::toolset,
        title = "{C}omputer {V}alidated {P}roofs of a {T}oolset for {A}daptable {A}rithmetic",
  author = "Marc Daumas and Claire Moreau-Finot and Laurent Th{\'e}ry",
  institution="INRIA Rhones-Alpes",
  type="Rapport de Recherche",
  number=4095,
  year = "2001",
                  month =jan
}

@ARTICLE {lt::Buchberger,
   AUTHOR = {Laurent Th{\'e}ry},
   TITLE = {A {M}achine-{C}hecked {I}mplementation of {B}uchberger's
            {A}lgorithm},
   JOURNAL = "Journal of Automated Reasoning",
   YEAR = {2001},
   VOLUME = {26},
   PAGES = {107--137}
}



@INPROCEEDINGS{MagaudBertot01,
  AUTHOR = {N. Magaud and Y. Bertot},
  TITLE = {{Changement de représentation des structures de données en Coq: le 
cas des entiers naturels}},
  BOOKTITLE = {JFLA'2001},
  YEAR = {2001},
  NOTE = {Also available as INRIA Research Report RR-4039},
  ABSTRACT = {Dans le calcul des constructions inductives, 
des outils de calcul et de preuve sont associés
à chaque type de données concret défini inductivement. Par conséquent, le 
choix d'une
structure de données influence fortement le contenu des preuves. 
Nous proposons dans ce document une méthode pour passer facilement
d'une représentation à une autre, en effectuant des traductions
partiellement automatisées des preuves.  Nous mettons cette méthode en
{\oe}uvre sur les entiers naturels, pour lesquels il existe une
représentation unaire (à la Peano) et une représentation binaire.
Un prototype d'outil de traduction est développé dans le système {C}oq et a été
expérimenté avec succès sur une dizaine de théorèmes d'arithmétique.},
  URL = {ftp://ftp-sop.inria.fr/lemme/Nicolas.Magaud/JFLA2001.ps.gz}
}
@INPROCEEDINGS{MagaudBertot00,
  AUTHOR = {N. Magaud and Y. Bertot},
  TITLE = {{Changing data structures in type theory: a study of natural 
numbers}},
  BOOKTITLE = {TYPES'2000},
  YEAR = {2001},
}






@article{gvo:setoids,
  author = {G. Barthe and V. Capretta and O. Pons},
  title = {Setoids in Type Theory},
  Journal=jfp,
  year = {2003}
}


@inproceedings{ascm01,
author ={H. Naciri and L. Rideau}, 
title ={FIGUE: Mathematical Formula Layout with Interaction and MathML Support.}, 
 booktitle = {The Fifth Asian Symposium on Computer Mathematics ASCM'2001},
 location={ Matsuyama, Japon}, 
 month={September},
 year = {2001}
}


@inproceedings{figueMathml01,
author ={ H. Naciri and L. Rideau}, 
 title= {The Mariage of MathML and Theorem Proving. },
 booktitle = {Internet Accessible Mathematical Computation Workshop 2001 (IAMC'2001)}, 
 month=jul,
 year=2001,
 location = {London Ontario, Canada}
}

@inproceedings{pcoq01,
 author ={Ahmed Amerkad and Yves Bertot and Laurence Rideau and Loïc Pottier},
 title = {Mathematics and proof presentation in Pcoq.},
 booktitle = {Workshop Proof Transformation and Presentation and Proof Complexities (PTP'01)},
 month=jun,
 year=2001,
 location ="Sienne,Italie",
note={Also appears as INRIA research report.}}

@techreport{figueMath,
 author ={ H. Naciri and L. Rideau}, 
 title={Affichage et manipulation interactive de formules mathématiques dans les documents structurés.},
        institution={Inria},
        year = {2001},
        month = {janvier},
        type = {Rapport de Recherche},
        number = {4140}
}

@inproceedings{gb01:agp,
  author = {G. Barthe and B. Ruiz Jiménez},
  title = {Principal types and semi-full closure for Extended Pure
                  Type Systems (In Spanish)},    
  year = {2001}
, Booktitle={Proceedings of AGP'01}
, Editor={L. Moniz Pereira and P. Quaresma}
}

@inproceedings{gt:cps,
  author = {G. Barthe and T. Uustalu},
  title = {CPS Translating Inductive and Coinductive Types},
  booktitle={Proceedings of PEPM'02},
  editor={P. Thiemann},
  publisher={ACM Press},
  year = {2002}}

@phdthesis{mh01,
 author={Marieke Huisman},
 title={Java program verification in higher order logic with PVS and Isabelle},
 school={University of Nijmegen},
 year={2001}} 



@phdthesis{Lavirotte:thesis,
 author={S. Lavirotte},
 title={Reconnaissance Structurelle de Formules Mathématiques Typographiées
         et Manuscrites},
 school={Université de Nice-Sophia Antipolis},
 year={2000}} 

@phdthesis{Coscoy:thesis,
 author={Y. Coscoy},
 title={Explication textuelle de preuves pour le calcul des constructions inductives},
 school={Université de Nice-Sophia Antipolis},
 year={2000}} 

@TECHREPORT{BPP2000,  author = {Y. Bertot and O. Pons and L. Pottier},
  institution= {INRIA}, 
  type = {Rapport de recherche},
  title = {Dependency graphs for interactive theorem provers},
  month={nov},year={2000}}



@INPROCEEDINGS{NaciriR,
        title           = "Affichage interactif, bidimensionnel et incrémental de formules mathématiques",
        author          = "H. Naciri and L. Rideau",
        booktitle       = "CARI'2000, ANTANANARIVO (Madagascar)",
        year            ="2000"}

@INPROCEEDINGS{Naciri,
        title           = "Conception et réalisation d'outils pour l'interaction homme machine dans les environnements de
démonstrations mathématiques.",
        author          = "H. Naciri",
        booktitle       = "JED'2000, Lyon",
        year            ="2000"}


@TECHREPORT{FDH,
  author = {C. Faure and J. Davenport and  H.Naciri},
  title = {Multi-valued Results in Computer Algebra.},
  institution = {INRIA},
  type = {Rapport de recherche},
  month = {Septembre},
  year = {2000},
  number = {RR-4007},
}
 
@INPROCEEDINGS{tphols2000,
        title           = "Fix-point Equations for Well-Founded Recursion in Type Theory",
        author          = "Antonia Balaa and Yves Bertot",
        pages           = "1--16",
        booktitle       = "Theorem Proving in Higher Order Logics",
        year            ="2000"}






@INPROCEEDINGS{XOT2000,
        author          = "C. Pasquier and L. Théry",
        title = "A Distributed Editing Environment for XML
Documents",
        booktitle= "actes de XOT2000 : premier Workshop ECOOP dédié
à XML et aux Technologies Objet, Cannes",
        year            = 2000,
        month = "juin"}



@INPROCEEDINGS{Stalmarck,
        crossref        = "tphols2000",
        title           = "Formalizing {S}t{\aa}lmarck's algorithm in {C}oq",
        author          = "Pierre Letouzey and Laurent Th{\'e}ry",
        pages           = "387--404"}





@inproceedings{LavirottePottier99,
AUTHOR = {Stéphane Lavirotte and Andrea Kosmala and Loïc Pottier and Gerard Rigoll},
TITLE = {On-Line Handwritten Formula Recognition using Hidden Markov Models and Context Dependent Graph Grammars},
BOOKTITLE = {ICDAR'99. Proceeding of Fifth International Conference on Document analysis and Recognition. Bangalore, India, september 1999."},
month = sep,
YEAR =  1999
}




@phdthesis{Pons99,
  author        = "Olivier Pons",
  title         = "{Conception et réalisation d'outils d'aide au
développement de grosses théories dans les systèmes de preuve interactifs}",
  school   = "Conservatoire National des
Arts et Métiers",
  year          = "1999",
  month         = "juillet",
  note          ="Thèse d'Université, effectuée sous la responsabilité de Laurence Rideau et Yves
Bertot"
}


@misc{Bertot99c,
  author        = "Yves Bertot",
  title         = "{Des environnements de preuve aux environnements de
programmation}",
  institution   = "Université de Nice-Sophia Antipolis",
  year          = "1999",
  month         = "octobre",
  note          ="Habilitation à diriger des recherches"
}


@inproceedings{cari02,
author ={ H. Naciri and L. Rideau}, 
title ={Affichage et diffusion sur Internet d'explications en langue arabe de preuves mathématiques}, 
booktitle = {CARI'2002 6ème Colloque Africain sur la Recherche en Informatique},
location={Yaoundé, Cameroun},
month={October},
year={ 2002}
} 

@inproceedings{MathML02,
author ={H. Naciri and  L. Rideau}, 
title ={Formal Mathematical Proof Explanations in Natural Language Using MathML: An Application to Proofs in Arabic}, 
 booktitle ={MathML International Conference 2002}, 
location={Chicago,USA}, 
month = { June},
year={ 2002 }
}



@Article{myars02,
  author = {A.~Armando and M.~Rusinowitch and S.~Stratulat},
  title = {Incorporating Decision Procedures in Implicit Induction},
  journal = {Journal of Symbolic Computation},
  year = 2002,
  volume = 34,
  number = 4,
  pages = {241-258}
}


@InProceedings{myiss02b,
  author = {A.~Imine and Y.~Slimani and S.~Stratulat},
  title = {Inductive Theorem Prover Based Verification of Concurrent Algorithms},
  booktitle = {MCSEAI02 (7th Maghrebian Conference on Computer Science)},
  pages = {313--324},
  year = 2002,
  volume = 2
}

@InProceedings{myiss02a,
  author = {A.~Imine and Y.~Slimani and S.~Stratulat},
  title = {Using Automated Induction-based Theorem Provers for Reasoning on  Concurrent Systems},
  booktitle = {JFPLC'2002 (Onzièmes Journées Francophones de Programmation Logique et Programmation par Contraintes)},
  pages = {71-85},
  year = 2002
}




@proceedings{appsem00,
  editor    = {Gilles Barthe and
               Peter Dybjer and
               Luis Pinto and
               Jo{\~a}o Saraiva},
  title     = {Applied Semantics, International Summer School, APPSEM 2000,
               Caminha, Portugal, September 9-15, 2000, Advanced Lectures},
  booktitle = {APPSEM},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2395},
  year      = {2002},
  isbn      = {3-540-44044-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}



@article{gt:fix,
  author =      {G. Barthe and T. Coquand},
  title = {On the equational theory of non-normalizing Pure Type Systems},
  journal= jfp,
  year =      {2003},
  note={To appear}
}



@article{g+:guard,
  author =      {G. Barthe and M. J. Frade  and E. Gim{\'e}nez and L. Pinto
                  and T. Uustalu},
  title =      {Type-Based Termination of Recursive Definitions},
  year =      {2003},
journal=mscs,
note={To appear}}


@article{gjm:wnsn,
author={G. Barthe and J. Hatcliff and M.H. S{\o}rensen},
title={{Weak Normalization implies Strong Normalization in Generalized
          Non-Dependent Pure Type Systems}},
year={2001},
month=oct,
journal=tcs,
pages={317--361},
volume={269},
number={1-2}}

@article{gjm:ip,
author={G. Barthe and J. Hatcliff and M.H.B. S{\o}rensen},
title={{An induction principle for Pure Type Systems}},
year={2001},
month=sep,
journal=tcs,
volume={266},
number={1-2},
pages={773-818}}

@inproceedings{g+02:amast,
  author =      {G. Barthe and P. Courtieu and G. Dufay and S. Melo
                  de Sousa}, 
  title = {{Tool-Assisted Specification and Verification
of the JavaCard Platform}},
  booktitle=amast02,
  editor={H. Kirchner and C. Ringessein},
  series=lncs,
  year = {2002},
  Publisher=springer,
  volume = 2422
}


@inproceedings{gt02:appsem,
  author =      {G. Barthe and T. Coquand},
  title =      {{An Introduction to Dependent Type Theory}},
  booktitle = {Applied Semantics. Lecture Notes for the APPSEM Summer 
School},
 editor={G. Barthe and P. Dybjer and L. Pinto and J. Saraiva},
  series=lncs,
  year = {2002},
  Publisher=springer,
  volume={2395}}

@inproceedings{gp02:tphols,
  author =      {G. Barthe and P. Courtieu}, 
  title = {{Efficient Reasoning about Executable Specifications in Coq}},
  booktitle={Proceedings of TPHOLs'02},
  editor={V.  Carre{\~n}o, C. Mu{\~n}oz and S. Tahar},
  series=lncs,
  year = {2002},
  Publisher=springer,
  volume={2xxx}}

@inproceedings{g+02:vmcai,
  author =      {G. Barthe and G. Dufay and L. Jakubiec and S. Melo
                  de Sousa},   
  title =      {{A formal correspondence between offensive and
                  defensive JavaCard virtual machines}},
  year =      {2002}
, Booktitle={Proceedings of VMCAI'02}
, Publisher=springer
, series= lncs
, volume= {2294}
, Editor= {A. Cortesi}
, pages={32--45}}






@inproceedings{gdm01:ftfjp,
  author =      {G. Barthe and D. Gurov and M. Huisman},
  title = {{Compositional specification and verification of control
                  flow based security properties of multi-application
                  programs}},  
  year =      {2001}
, Booktitle={Proceedings of FTfJP'01}
, Editor= {S. Drossopoulou et al}
}



@inproceedings{g+01:esmart,
  author =      {G. Barthe and G. Dufay and M. Huisman and S. Melo de 
Sousa},
  title = {{Jakarta: a toolset to reason about the JavaCard platform}},
  year =      {2001}
, Booktitle={Proceedings of e-SMART'01}
, Publisher=springer
, series= lncs
, volume= {2140}
, pages={2--18}
, editor= {I. Attali and T. Jensen}

}

@inproceedings{go01:fossacs,
  author =      {G. Barthe and O. Pons},
  title = {{Type Isomorphisms and Proof Reuse in Dependent Type Theory}},
  year =      {2001}
, Booktitle={Proceedings of FOSSACS'01}
, Publisher=springer
, series= lncs
, volume= {2030}
, Editor= {F. Honsell and M. Miculan}
, pages={57--71}
}


@inproceedings{g+01:esop,
  author =      {G. Barthe and G. Dufay and L. Jakubiec and
                  B. Serpette  and S. Melo de Sousa}, 
  title =      {{A Formal Executable Semantics of the JavaCard Platform}},
  year =      {2001}
, Booktitle={Proceedings of ESOP'01}
, Publisher=springer
, series= lncs
, volume= {2028}
, Editor= {D. Sands}
, pages={302--319}}

@misc{BertotCasteran03,
  author = "Yves Bertot and Pierre Castéran",
  title = "Le Coq'Art",
  note = "book to appear, available at
     {\tt http://www-sop.inria.fr/lemme/Yves.Bertot/coqart.html}",
  year = 2002
}


@inproceedings{BalaaBertot02,
title = "Fonctions récursives générales par itération en théorie des
types",
author = "Antonia Balaa and Yves Bertot",
booktitle = {\sl Journ{\'e}es Francophones pour les Langages Applicatifs},
month = jan,
year = 2002,
}

@inproceedings{Bertot02,
author = "Yves Bertot",
title = "Des descriptions fonctionnelles aux implémentations impératives de programmes",
booktitle ={\sl Journ{\'e}es francophones pour les langages applicatifs, JFLA'02},
month = jan,
year = 2002,
note = {en Fran{\c{c}}ais}
}

@inproceedings{tphols2002-BertotCaprettaDasBarman,
   author= "Yves Bertot and Venanzio Capretta and Kuntal Das Barman",
   title = "Type-theoretic functional semantics",
   booktitle = {Theorem Proving in Higher Order Logics (TPHOLS'02)},
   year = 2002,
   month = aug,
   location = "Hampton, Va",
  series = "LNCS",
  publisher = "Springer-Verlag",
  number = 2410
}



@InProceedings{courtieufmppta02,
  author = {Pierre Courtieu},
  title = {Proving self-stabilization with a proof assistant},
  booktitle = {Proceedings of IPDPS'2002},
  series =       {IEEE CS Press},
  year = {2002}
}


@Article{BeMaZi03,
  author = {Yves Bertot and Nicolas Magaud and Paul Zimmermann},
  title = {A {GMP} program computing square roots and its proof within 
{C}oq},
  journal = {Journal of Automated Reasoning},
  year = 2003,
  note = {To appear. Special Issue on Automating and Mechanising Mathematics: 
In honour of N.G. de Bruijn}
}
@InProceedings{BartheGH02,
  author =       "G. Barthe and D. Gurov and M. Huisman",
  title =        "Compositional Verification of Secure Applet 
Interactions",
  booktitle =    "Proc.\ FASE'02",
  PUBLISHER  = springer,
  series =       lncs,
  number =       "2306",
  pages =        "15--32",
  year =         "2002",
  editor = "R.-D. Kutsche and H. Weber"

}


@inproceedings{TrentelmanH02,
title = {{Extending JML Specifications with Temporal Logic}},
author = "K. Trentelman and M. Huisman",
year = 2002,
booktitle = amast02,
publisher = springer,
series = lncs,
pages = "334-348",
number = 2422,
editor = "H. Kirchner and C. Ringeissen"
}

@inproceedings{CatanoH02a,
title = {Formal Specification and Static Checking of {Gemplus's} 
Electronic Purse Using {ESC/Java}},
author = "N. Cata{\~n}o and M. Huisman",
year = 2002,
booktitle = fme02,
editor = "L.-H. Eriksson and P.A. Lindsay",
series = lncs,
publisher = springer,
number = "2391",
pages = "272--289"
}

@INPROCEEDINGS{Huisman02,
author = "M. Huisman",
title = "{Verification of Java's AbstractCollection class: a case 
study}",
booktitle = "Mathematics of Program Construction (MPC'02)",
number = 2386,
series = lncs,
pages = "175 - 194",
publisher = springer,
year = 2002,
editor = "E. Boiten and B. M{\"o}ller"
}


@INPROCEEDINGS{lplc02,
        title           = "Mathematical quotients and quotient types in Coq",
        author          = "L. Chicli and  L. Pottier and C. Simpson",
   booktitle =    "TYPES Workshop ",
        publisher =    "submitted to LNCS",
        address =      "Berg en Dal, Netherlands",
        year =         "2002",
}
@TECHREPORT{fg02,
  author = {Fr\'ed\'erique Guilhot},
  title = {Proofs with Coq of theorems in plane geometry using oriented angles},
  institution = {INRIA},
  type = {Rapport de recherche},
  year = {2002},
  number = {RR-4356},
}
@phdthesis{capretta:2002,
  author     = "Venanzio Capretta",
  title      = "Abstraction and Computation",
  school     = "Computing Science Institute, University of Nijmegen",
  year       = 2002
}