@Misc{ocaml,
  key = 	 {OCaml},
  OPTauthor = 	 {},
  title = 	 {{Le langage de programmation Objective Caml}},
  howpublished = {\url{http://caml.inria.fr/ocaml}},
  OPTmonth = 	 {},
  OPTyear = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{cic,
  author = 	 {Yves Bertot and Pierre Castéran},
  ALTeditor = 	 {},
  title = 	 {Interactive Theorem Proving and Program Development. Coq'Art : The Calculus of Inductive Constructions},
  publisher = 	 {Springer Verlag},
  year = 	 {2004},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  series = 	 {Texts in Theoretical Computer science, EATCS},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  month = 	 {03},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@InProceedings{lo,
  author = 	 {Sungwoo Park and Frank Pfenning and Sebastian Thrun},
  title = 	 {A Probabilistic Language based upon Sampling Functions},
  OPTcrossref =  {},
  OPTkey = 	 {},
  booktitle = {POPL'05},
  OPTpages = 	 {},
  year = 	 {2005},
  OPTeditor = 	 {},
  OPTvolume = 	 {},
  OPTnumber = 	 {},
  OPTseries = 	 {},
  OPTaddress = 	 {},
  month = 	 {01},
  organization = {ACM},
  OPTpublisher = {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@TechReport{filliatre,
  author = 	 {Jean-Christophe Filliâtre},
  title = 	 {Proof of Imperative Programs in Type Theory},
  institution =  {LRI CNRS Université Paris Sud Orsay},
  year = 	 {},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTnumber = 	 {},
  OPTaddress = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@PhdThesis{hurd,
  author = 	 {Joe Hurd},
  title = 	 {Formalizing Mathematics to Verify Probabilistic Algorithms},
  school = 	 {Trinity College, University of Cambridge},
  year = 	 {2001},
  OPTkey = 	 {},
  OPTtype = 	 {},
  OPTaddress = 	 {},
  month = 	 {08},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Book{markov,
  author = 	 {Bernard Ycart},
  OPTeditor = 	 {},
  title = 	 {Modèles et Algorithmes Markoviens},
  publisher = 	 {Springer Verlag},
  year = 	 {2002},
  OPTkey = 	 {},
  OPTvolume = 	 {},
  number = 	 {39},
  series = 	 {Société de Mathématiques Appliquées et Industrielles, coll. Mathématiques et Applications},
  OPTaddress = 	 {},
  OPTedition = 	 {},
  OPTmonth = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}


@Misc{coq,
  key = 	 {Coq},
  OPTauthor = 	 {},
  title = 	 {{Le système d'aide à la preuve Coq.}},
  howpublished = {\url{http://coq.inria.fr}}},
  OPTmonth = 	 {},
  OPTyear = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Misc{why,
  key = 	 {Why},
  OPTauthor = 	 {},
  title = 	 {{L'outil de vérification formelle de logiciels Why}},
  howpublished = {\url{http://why.lri.fr}}},
  OPTmonth = 	 {},
  OPTyear = 	 {},
  OPTnote = 	 {},
  OPTannote = 	 {}
}

@Article{hoare,
  author = 	 {C. A. R. Hoare},
  title = 	 {An Axiomatic Basis for Computer Programming},
  journal = 	 {Communications of the ACM},
  year = 	 {1969},
  OPTkey = 	 {},
  volume = 	 {12},
  number = 	 {10},
  OPTpages = 	 {},
  month = 	 {10},
  OPTnote = 	 {},
  OPTannote = 	 {}
}