@article{Lumbroso2013arxiv,
  author    = {J{\'e}r{\'e}mie Lumbroso},
  title     = {Optimal Discrete Uniform Generation from Coin Flips, and Applications},
  journal   = {CoRR},
  volume    = {abs/1304.1916},
  year      = {2013},
  url       = {http://arxiv.org/abs/1304.1916},
}

@book{McIverMorgan2005,
  author = {Annabelle McIver and Carroll Morgan},
  title = {Abstraction, Refinement and Proof for Probabilistic Systems},
  series = {Monographs in Computer Science},
  year = 2005,
  publisher = {Springer},
}

@inproceedings{Hurd2002TPHOLs,
  author = {Joe Hurd},
  title = {A Formal Approach to Probabilistic Termination},
  year = {2002},
  editor_long = {Victor A. Carre{\~n}o and C{\'e}sar A. Mu{\~n}oz and Sofi{\'e}ne Tahar},
  booktitle_long = {Theorem Proving in Higher Order Logics (TPHOLs 2002)},
  booktitle = {TPHOLs 2002},
  volume = {2410},
  series = {LNCS},
  doi = {10.1007/3-540-45685-6_16},
  publisher = {Springer},
  pages = {230--245},
}
