Thibault Gauthier   

Research

Aligning Concepts across Proof Assistant Libraries (to appear) [pdf]
Source code and data from the experiments are available here.
This work improves on "Matching concepts across HOL libraries".
Learning to Reason with HOL4 tactics [pdf, bibtex]
Included in HOL4 github repository. See src/tactictoe/README.
Results of the experiments are available here.
Sharing HOL4 and HOL Light proof knowledge [pdf, bibtex]
Matching concepts across HOL libraries [pdf, bibtex]
Results of the experiments are available here.
Premise Selection and External Provers for HOL4 [pdf, bibtex]
Included in HOL4 github repository. See src/holyhammer/README.
Beagle as a HOL4 external ATP method [pdf, bibtex]
An experimental version is available here.