[PL-sem-jr] Talk tomorrow, 11/30

[Aaron Turon]

Monday, 11/30, WVH164, 11:30-1:30

Speaker: Vasilis

A taste of Co{C,q}

This talk is about theorem proving based on type theory. I will start
by providing intuition about intuitionistic logic. I will discuss
different typed lambda calculi and their relations to systems of logic
aided by Barendregt's cube. Finally, I will attempt to introduce you
to Coq, a proof assistant based on the Calculus of Inductive
Constructions.