Divasón, Jose (2018). "A Formalization of the LLL Basis Reduction Algorithm". Interactive Theorem Proving: 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018, Proceedings. Lecture Notes in Computer Science. Vol. 10895. pp. 160–177. doi:10.1007/978-3-319-94821-8_10. ISBN978-3-319-94820-1.