\@addtocsec{htoc}{1}{0}{\@print{1}\quad{}Major scientific results} \@addtocsec{htoc}{2}{1}{\@print{1.1}\quad{}Correctness of Computer Systems} \@addtocsec{htoc}{3}{1}{\@print{1.2}\quad{}Formal Mathematics and Mathematics Education} \@addtocsec{htoc}{4}{1}{\@print{1.3}\quad{}Proof Technology} \@addtocsec{htoc}{5}{1}{\@print{1.4}\quad{}Foundational Research} \@addtocsec{htoc}{6}{0}{\@print{2}\quad{}Cooperation with industry} \@addtocsec{htoc}{7}{0}{\@print{3}\quad{}List of visitors from other sites} \@addtocsec{htoc}{8}{1}{\@print{3.1}\quad{}URL} \@addtocsec{htoc}{9}{0}{\@print{4}\quad{}List of publications} \bibcite{conchon-krstic-04}{1} \bibcite{contejean05jar}{2} \bibcite{marche04jlap}{3} \bibcite{marche2004jsc}{4} \bibcite{krstic-conchon-04}{5} \bibcite{andronick05fm}{6} \bibcite{contejean05cade}{7} \bibcite{filliatre04icfem}{8} \bibcite{hubert05sefm}{9} \bibcite{jacobs04amast}{10} \bibcite{marche05tphols}{11} \bibcite{monin04tphols}{12} \bibcite{oury05tphols}{13} \bibcite{ayache05master}{14} \bibcite{corbineau05these}{15} \bibcite{hubert04dea}{16} \bibcite{sozeau05master}{17} \bibcite{CoqManualV8}{18} \bibcite{tphols2005}{19}