has been a subject of active research since then; see the monograph of Jacobs (1999) for instance. Homotopy type theory attempts to combine type theory and category theory. It focuses on equalities, especially equalities between types. List of type theories Major Simply typed lambda calculus which is a higher-order logic intuitionistic type theory system F LF is often used to define other type theories calculus of constructions and its derivatives Minor Automath ST type theory UTT (Luo's Unified Theory of dependent Types) some forms of combinatory logic others defined in the lambda cube (also known as pure type systems) others under the name typed lambda calculus Active research Homotopy type theory explores equality of types Cubical Type Theory is an implementation of homotopy type theory Applications Mathematical foundations The first computer proof assistant, called Automath, used type theory to encode mathematics on a computer. Martin-Löf specifically developed intuitionistic type theory to encode all mathematics to serve as a new foundation for mathematics. There is ongoing research into mathematical foundations using homotopy type theory. Mathematicians working in category theory already had difficulty working with the widely accepted foundation of Zermelo–Fraenkel set theory. This led to proposals such as Lawvere's Elementary Theory of the Category of Sets (ETCS). Homotopy type theory continues in this line using type theory. Researchers are exploring connections between dependent types (especially the identity type) and algebraic topology (specifically homotopy). Proof assistants Much of the current research into type theory is driven by proof checkers, interactive proof assistants, and automated theorem provers. Most of these systems use a type theory as the mathematical foundation for encoding proofs, which is not surprising, given the close connection between type theory and programming languages: LF is used by Twelf, often to define other type theories; many type theories which fall under higher-order logic are used by the HOL family of provers and PVS; computational type theory is used by NuPRL; calculus of constructions and its derivatives are used by Coq, Matita, and Lean; UTT (Luo's Unified Theory of dependent Types) is used by Agda which is both a programming language and proof assistant Many type theories are supported by LEGO and Isabelle. Isabelle also supports foundations besides type theories, such as ZFC. Mizar is an example of a proof system that only supports set theory. Programming languages Any static program analysis, such as the type checking algorithms in the semantic analysis