Accepted at CADE-28, 2021
Accepted in International Journal on Software Tools for Technology Transfer, 20xy
Practical Aspects of Automated Reasoning (PAAR-2020), 2020
In Ariola, Z.M. (ed.), 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), LIPIcs 167, pp. 5:1–5:17, Schloss Dagstuhl—Leibniz-Zentrum für Informatik, 2020
In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 495–507, Springer, 2019
In Fontaine, P. (ed.) 27th International Conference on Automated Deduction (CADE-27), LNCS 11716, pp. 55–73, Springer, 2019
In Vojnar, T., Zhang, L. (eds.) 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), LNCS 11427, pp. 192–210, Springer, 2019
In the last two years I have been the main developer of the Zipperposition theorem prover. It is a well-performing polymorphic higher-order theorem prover. Unlike other provers like E or Vampire, Zipperposition does not have an auto mode. Therefore, if you would like to use it in your projects let me know and I will provide you with a reasonable configuration to use in your domain.
You can find Zipperposition at the following link
I am also the main developer behind Ehoh, an extension of E to a fragment of higher-order logic. An extension to full higher-order logic is planned.
You can find E at the following link