F. Alessi, A. Ciaffaglione, P. Di Gianantonio, F. Honsell, M. Lenisa, and I. Scagnetto, “LF+ in Coq for "fast and loose" reasoning”, JFR, vol. 12, no. 1, pp. 11–51, Jan. 2019.