A Basic Extended Simple Type Theory William M. Farmer 9 June 2004 Abstract 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.