@inproceedings{ITP19,
  author = {Johannes \AA{}man Pohjola and
            Henrik Rostedt and
            Magnus O. Myreen},
  title = {Characteristic Formulae for Liveness Properties of Non-terminating {CakeML} Programs},
  year = 2019,
  booktitle = {Interactive Theorem Proving ({ITP})},
  publisher = {LIPIcs},
  url = {https://cakeml.org/itp19.pdf}
}

@article{Coinductive-AFP,
  author  = {Andreas Lochbihler},
  title   = {Coinductive},
  journal = {Archive of Formal Proofs},
  month   = {February},
  year    = {2010},
  note    = {\url{https://isa-afp.org/entries/Coinductive.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
