@inproceedings{coherent,
  author    = {Coquand, Thierry and M\"ortberg, Anders and Siles, Vincent},
  title     = {{Coherent and Strongly Discrete Rings in Type Theory}},
  keywords  = {Formalization of mathematics; Constructive algebra; Coq; SSReflect},
  booktitle = {Certified Programs and Proofs},
  series    = {Lecture Notes in Computer Science},
  year      = {2012},
  volume    = {7679},
  pages     = {273-288},
  isbn      = {978-3-642-35307-9},
  editor    = {Hawblitzel, Chris and Miller, Dale},
  doi       = {10.1007/978-3-642-35308-6_21},
  url       = {http://dx.doi.org/10.1007/978-3-642-35308-6_21},
  publisher = {Springer Berlin Heidelberg},
}