Ansten Klev (Mar 5 and Mar 12)
Section outline
-
In my two lectures I will introduce you to type theory, which is a general form of language that includes propositional and predicate logic and that lies at the basis of many programming languages. My presentation will (of course) be coloured by my own interests, which tend to be philosophical. I will start by explaining, in very general terms, what a type is and then define, for the purposes of illustration, a simple type theory. The second lecture will be devoted to the Curry–Howard correspondence, by means of which logic is included in type theory. I will try to explain to you what a dependent type is and why dependent types are useful for the formalization of the universal quantifier ("for all x").