Interactive Theorem Proving 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings - Ayala-Rincón, Mauricio; Muñoz, César A. (Springer International Publishing : Imprint: Springer, 2017)