@InProceedings{prevosto:DSP:2005:274,
  author =      {Virgile Prevosto},
  title =       {Certified mathematical hierarchies: the FoCal system},
  booktitle =   {Mathematics, Algorithms, Proofs},
  year =        {2005},
  editor =      {Thierry Coquand and Henri Lombardi and Marie-Fran{\\c{c}}oise Roy},
  number =      {05021},
  series =      {Dagstuhl Seminar Proceedings},
  publisher =   {Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany},
  address =  {Dagstuhl, Germany},
  annote =   {Keywords: Specifications, proofs, inheritance, refinement, types, Focal, Coq, computer algebra, mathematics}}