, Department of Mathematics, Ohio State University, Columbus OH 43210, USA, United States
-
Journal of Formalized Reasoning Vol. 9 No. 1 (2016): Special Issue: Twenty Years of the QED Manifesto - QED 20th anniversary
Conversion of HOL Light proofs into Metamath
Abstract PDF