Speaker: |
Piyush Kurur (Indian Institute of Technology Department of Computer Science and Engineering Kanpur 208016 And Visiting Professor School of Technology and Computer Science TIFR, Mumbai) |

Organiser: |
Paritosh K Pandya |

Date: |
Monday, 25 Apr 2016, 16:00 to 17:00 |

Venue: |
A-201 (STCS Seminar Room) |

(Scan to add to calendar)

A proof assistant is a program that checks a formal proof for correctness. It turns out that verifying mathematical proofs are closely connected to checking types in a sufficiently sophisticated programming language. This connection goes by the name Curry-Howard isomorphism although several others have independently made the above connection. One of the goals of my talk is to give an overview of this deep connection.

Having introduced the basics of type theory, I will look at the exciting new developments in this area: the theory of homotopy types and univalent foundation.

I will try to make this talk as self contained as possible. In particular no background on programming languages, type theory or homotopy theory will be assumed.