bibliographer - John Harrison

bibliographer a curated TCS bibliography

obsidian
tags
authors
no doi
no pdf
bad author
add item
librarian

Some new results on decidability for elementary algebra and geometry Robert M. Solovay R.D. Arthan John Harrison [github]

History of Interactive Theorem Proving John Harrison Josef Urban Freek Wiedijk [github]

A Revision of the Proof of the Kepler Conjecture Thomas C. Hales John Harrison Sean McLaughlin Tobias Nipkow Steven Obua Roland Zumkeller [github]

HOL Light: An Overview John Harrison [github]

A mizar mode for HOL John Harrison [github]

The HOL Light Theory of Euclidean Space John Harrison [github]

A FORMAL PROOF OF THE KEPLER CONJECTURE THOMAS HALES MARK ADAMS GERTRUD BAUER TAT DAT DANG JOHN HARRISON LE TRUONG HOANG CEZARY KALISZYK VICTOR MAGRON SEAN MCLAUGHLIN TAT~THANG NGUYEN QUANG TRUONG NGUYEN TOBIAS NIPKOW STEVEN OBUA JOSEPH PLESO JASON RUTE ALEXEY SOLOVYEV THI HOAI AN TA NAM TRUNG TRAN THI DIEP TRIEU JOSEF URBAN KY VU ROLAND ZUMKELLER [github]

Library Size: 13G (7 entries), Last Updated: Apr 04, 2026, 18:14:59, Build Time: N/A

[show logs] [hide logs]