@inproceedings(DBLP:conf/pkdd/AugerCT13,
 author       = {David Auger and Adrien Cou{\"{e}}toux and Olivier Teytaud},
 year         = {2013},
 title        = {Continuous Upper Confidence Trees with Polynomial Exploration - Consistency},
 booktitle    = {Machine Learning and Knowledge Discovery in Databases - European Conference, {ECML} {PKDD} 2013, Prague, Czech Republic, September 23-27, 2013, Proceedings, Part {I}},
 pages        = {194--209},
 doi          = {10.1007/978-3-642-40988-2\_13},
)
@inproceedings(DBLP:conf/icml/BansalLRSW19,
 author       = {Kshitij Bansal and Sarah M. Loos and Markus N. Rabe and Christian Szegedy and Stewart Wilcox},
 year         = {2019},
 title        = {HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving},
 editor       = {Kamalika Chaudhuri and Ruslan Salakhutdinov},
 booktitle    = {Proceedings of the 36th International Conference on Machine Learning, {ICML} 2019, 9-15 June 2019, Long Beach, California, {USA}},
 series       = {Proceedings of Machine Learning Research},
 volume       = {97},
 publisher    = {{PMLR}},
 pages        = {454--463},
 url          = {http://proceedings.mlr.press/v97/bansal19a.html},
)
@inproceedings(coq,
 author       = {Yves Bertot},
 year         = {2008},
 title        = {A Short Presentation of {C}oq},
 editor       = {Otmane Ait Mohamed and Mu\IeC{\~n}oz, C\IeC{\'e}sar and Sofi\IeC{\`e}ne Tahar},
 booktitle    = {Conference on Theorem Proving in Higher Order Logics (TPHOLs)},
 series       = {LNCS},
 volume       = {5170},
 publisher    = {Springer},
 pages        = {12--16},
 doi          = {10.1007/978-3-540-71067-7_3},
)
@inproceedings(DBLP:conf/mkm/BlaauwbroekUG20,
 author       = {Lasse Blaauwbroek and Josef Urban and Herman Geuvers},
 year         = {2020},
 title        = {The Tactician - {A} Seamless, Interactive Tactic Learner and Prover for Coq},
 editor       = {Christoph Benzm{\"{u}}ller and Bruce R. Miller},
 booktitle    = {Intelligent Computer Mathematics - 13th International Conference, {CICM} 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings},
 series       = {LNCS},
 volume       = {12236},
 publisher    = {Springer},
 pages        = {271--277},
 doi          = {10.1007/978-3-030-53518-6\_17},
)
@inproceedings(DBLP:conf/cade/ChvalovskyJ0U19,
 author       = {Karel Chvalovsk{\'{y}} and Jan Jakubuv and Martin Suda and Josef Urban},
 year         = {2019},
 title        = {{ENIGMA-NG:} Efficient Neural and Gradient-Boosted Inference Guidance for {E}},
 booktitle    = {Automated Deduction - {CADE} 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings},
 pages        = {197--215},
 doi          = {10.1007/978-3-030-29436-6\_12},
)
@inproceedings(DBLP:conf/lpar/Gauthier20,
 author       = {Thibault Gauthier},
 year         = {2020},
 title        = {Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic},
 editor       = {Elvira Albert and Laura Kov{\'{a}}cs},
 booktitle    = {{LPAR} 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020},
 series       = {EPiC Series in Computing},
 volume       = {73},
 publisher    = {EasyChair},
 pages        = {230--248},
 doi          = {10.29007/7jmg},
)
@inproceedings(DBLP:conf/mkm/Gauthier20,
 author       = {Thibault Gauthier},
 year         = {2020},
 title        = {Tree Neural Networks in {HOL4}},
 editor       = {Christoph Benzm{\"{u}}ller and Bruce R. Miller},
 booktitle    = {Intelligent Computer Mathematics - 13th International Conference, {CICM} 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings},
 series       = {LNCS},
 volume       = {12236},
 publisher    = {Springer},
 pages        = {278--283},
 doi          = {10.1007/978-3-030-53518-6\_18},
)
@article(DBLP:journals/jar/GauthierKUKN21,
 author       = {Thibault Gauthier and Cezary Kaliszyk and Josef Urban and Ramana Kumar and Michael Norrish},
 year         = {2021},
 title        = {TacticToe: Learning to Prove with Tactics},
 journal      = {J. Autom. Reason.},
 volume       = {65},
 number       = {2},
 pages        = {257--286},
 doi          = {10.1007/s10817-020-09580-x},
)
@inproceedings(hollight,
 author       = {John Harrison},
 year         = {2009},
 title        = {{HOL Light}: An Overview},
 editor       = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
 booktitle    = {Conference on Theorem Proving in Higher Order Logics (TPHOLs)},
 series       = {LNCS},
 volume       = {5674},
 publisher    = {Springer},
 pages        = {60--66},
 doi          = {10.1007/978-3-642-03359-9_4},
)
@inproceedings(hurd05,
 author       = {Joe Hurd},
 year         = {2005},
 title        = {System Description: {T}he {M}etis Proof Tactic},
 editor       = {Carsten Schuermann Christoph Benzmueller, John Harrison},
 booktitle    = {Workshop on Empirically Successful Automated Reasoning in Higher-Order Logic (ESHOL)},
 pages        = {103--104},
 url          = {https://arxiv.org/pdf/cs/0601042},
)
@inproceedings(DBLP:conf/nips/KaliszykUMO18,
 author       = {Cezary Kaliszyk and Josef Urban and Henryk Michalewski and Miroslav Ols{\'{a}}k},
 year         = {2018},
 title        = {Reinforcement Learning of Theorem Proving},
 editor       = {Samy Bengio and Hanna M. Wallach and Hugo Larochelle and Kristen Grauman and Cesa{-}Bianchi, Nicol{\`{o}} and Roman Garnett},
 booktitle    = {Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montr{\'{e}}al, Canada},
 pages        = {8836--8847},
 url          = {https://proceedings.neurips.cc/paper/2018/hash/55acf8539596d25624059980986aaa78-Abstract.html},
)
@inproceedings(DBLP:conf/kbse/NagashimaH18,
 author       = {Yutaka Nagashima and Yilun He},
 year         = {2018},
 title        = {{PaMpeR}: proof method recommendation system for {Isabelle/HOL}},
 editor       = {Marianne Huchard and Christian K{\"{a}}stner and Gordon Fraser},
 booktitle    = {Proceedings of the 33rd {ACM/IEEE} International Conference on Automated Software Engineering, {ASE} 2018, Montpellier, France, September 3-7, 2018},
 publisher    = {{ACM}},
 pages        = {362--372},
 doi          = {10.1145/3238147.3238210},
)
@article(silver2017mastering,
 author       = {David Silver and Julian Schrittwieser and Karen Simonyan and Ioannis Antonoglou and Aja Huang and Arthur Guez and Thomas Hubert and Lucas Baker and Matthew Lai and Adrian Bolton and Yutian Chen and Timothy Lillicrap and Fan Hui and Laurent Sifre and George van den Driessche and Thore Graepel and Demis Hassabis},
 year         = {2017},
 title        = {Mastering the game of {G}o without human knowledge},
 journal      = {Nature},
 volume       = {550},
 pages        = {354--359},
 doi          = {10.1038/nature24270},
)
@inproceedings(hol4,
 author       = {Konrad Slind and Michael Norrish},
 year         = {2008},
 title        = {A Brief Overview of {HOL4}},
 editor       = {Otmane A\"{\i}t Mohamed and Mu{\~n}oz, C{\'e}sar A. and Sofi{\`e}ne Tahar},
 booktitle    = {Conference on Theorem Proving in Higher Order Logics (TPHOLs)},
 series       = {LNCS},
 volume       = {5170},
 publisher    = {Springer},
 pages        = {28--32},
 doi          = {10.1007/978-3-540-71067-7_6},
)
@inproceedings(isabelle,
 author       = {Makarius Wenzel and Lawrence C. Paulson and Tobias Nipkow},
 year         = {2008},
 title        = {The {I}sabelle Framework},
 editor       = {Otmane A\"{\i}t Mohamed and Mu{\~n}oz, C{\'e}sar A. and Sofi{\`e}ne Tahar},
 booktitle    = {Conference on Theorem Proving in Higher Order Logics (TPHOLs)},
 series       = {LNCS},
 volume       = {5170},
 publisher    = {Springer},
 pages        = {33--38},
 doi          = {10.1007/978-3-540-71067-7_7},
)