Speaker : Balaji R Rao
Date : 27th May, 2014 (Tuesday)
Time : 09:00 pm – 10:00 pm
Venue : Lecture Hall I, Department of Mathematics
Abstract : Type theory offers an alternate foundation for mathematics. Unlike in set theory, where everything is a set, in type theory, objects are of different ‘types’. Type theory based foundations aim to be closer to actual mathematical practice than traditional foundations. Though ZFC (based on predicate calculus) has been the accepted foundation for several years, a working mathematician rarely cares about how her theorems and constructions translate into ZFC.
Type theory, being essentially computational in nature, has been the basis of several programming languages, of which Agda is an example. The link between programming languages and proofs is the ‘propositions-as-types’ principle, which allows proofs to be expressed as programs, which computers are good at checking.
In this talk we provide an introduction to type theory and Agda. Though useful, familiarity with computer programming is not assumed.
Area: Type Theory