A Basic Extended Simple Type Theory
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.