Characteristic Formulae for Liveness Properties of Non-Terminating CakeML Programs. - Johannes Åman Pohjola; Henrik Rostedt; Magnus O. Myreen (ITP, 2019)