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.
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
