1. A FORMAL PROOF OF THE KEPLER CONJECTURE. (29th May 2017) Authors: HALES, THOMAS; ADAMS, MARK; BAUER, GERTRUD; DANG, TAT DAT; HARRISON, JOHN; HOANG, LE TRUONG; KALISZYK, CEZARY; MAGRON, VICTOR; MCLAUGHLIN, SEAN; NGUYEN, TAT THANG; NGUYEN, QUANG TRUONG; NIPKOW, TOBIAS; OBUA, STEVEN; PLESO, JOSEPH; RUTE, JASON; SOLOVYEV, ALEXEY; TA, THI HOAI AN; TRAN, NAM TRU... Journal: Forum of mathematics Issue: Volume 5(2017) Page Start: Record Type: Journal Article View Content: Available online (eLD content is only available in our Reading Rooms) ↗
2. Verified decision procedures for MSO on words based on derivatives of regular expressions. (2015) Authors: TRAYTEL, DMITRIY; NIPKOW, TOBIAS Journal: Journal of functional programming Issue: Volume 25(2015) Page Start: Record Type: Journal Article View Content: Available online (eLD content is only available in our Reading Rooms) ↗
3. Verified decision procedures for MSO on words based on derivatives of regular expressions. (5th November 2015) Authors: TRAYTEL, DMITRIY; NIPKOW, TOBIAS Journal: Journal of functional programming Issue: Volume 25(2015) Page Start: Record Type: Journal Article View Content: Available online (eLD content is only available in our Reading Rooms) ↗