Typetheorie

In de wiskunde, logica en informatica houdt de typetheorie zich bezig met formele typesystemen. Sommige typesystemen kunnen dienen als grondslagen van de wiskunde, als alternatief voor de verzamelingenleer. Voorbeelden van typesystemen zijn de getypeerde lambdacalculus en intuïtionistische typetheorie.

Sommige informatici beschouwen ook het ontwerp, de analyse en het gebruik van datatypes, die in programmeertalen gebruikt worden, als onderdeel van de typetheorie. De meeste bewijsassistenten gebruiken ook typetheorie, voorbeelden hiervan zijn Coq, Agda en Lean. De voorloper Automath gebruikte typetheorie voor de bewijschecker.