Talking head
LambdaConf 2015

Traditionally, in Computer Science, sets are assumed to be the basis of a type theory, together with Boolean logic. In this version of type theory, we do not need sets or Boolean logic; intuitionism is enough ("no principle of excluded middle required"). The underlying math is Topos Theory, but you are not required to be even aware of its existence. The theory is described using diagrams, not the traditional (and tricky) deduction rules. The resulting theory turns out to have dependent types. A simple "real-life" example or two will illustrate all this.

Rated: Everyone
Viewed 95 times
Tags: There are no tags for this video.