This paper presents an extended version
of Church’s simple type theory called Basic Extended Simple Type Theory
(bestt). By adding type variables and support for reasoning with tuples, lists,
and sets to
simple type theory, it is intended to be
a practical logic for formalized mathematics.