An introduction to Type Theory through Agda

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


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s