 An selection of theorem provers for Church’s type theory is presented. The focus is on systems that have successfully participated in TPTP THF CASC competitions in the past. The latest editions of most mentioned systems can be accessed online via the SystemOnTPTP infrastructure (Sutcliffe 2017). Nearly all mentioned systems produce verifiable proof certificates in the TPTP TSTP syntax. Further details on the automation of Church’s type theory are given in Benzmüller &amp; Miller 2014.