@techreport{Barras96a,
   author = {B.~Barras},
   title = {Coq en Coq},
   institution = {INRIA},
   number = {3026},
   type = {Rapport de Recherche},
   month = oct,
   year = {1996}}



@InProceedings{Barras96b,
  author =       {B.~Barras},
  title =        {Verification of the Interface of a Small Proof
                  System in Coq},
  editor =       {E.~Gimenez and C.~Paulin-Mohring},
  booktitle =    {Proceedings of the 1996 Workshop on Types
                  for Proofs and Programs},
  publisher =    {Springer-Verlag LNCS 1512},
  address =      {Aussois, France},
  month =        dec,
  year =         {1996},
  pages =        {28--45}
}



@PHDTHESIS{Barras99,
  AUTHOR = {B.~Barras},
  TITLE = {Auto-validation d'un syst{\`e}me de preuves avec familles
           inductives},
  TYPE = {Th{\`e}se de Doctorat},
  SCHOOL = {Universit{\'e} Paris~7},
  YEAR = 1999,
  MONTH = nov
}