Tata Institute of Fundamental Research
Types, Proofs and Homotopy
STCS Seminar
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)
Abstract:
Abstract: In many programming languages, values have an associated type that the compilers enforces. For example, adding a value of type INTEGER to a value of type STRING will be flagged as an error by these compilers. Such checks by the compiler helps in eliminating a large class of bugs that arise in practice.
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.
| 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)
Abstract:
Abstract: In many programming languages, values have an associated type that the compilers enforces. For example, adding a value of type INTEGER to a value of type STRING will be flagged as an error by these compilers. Such checks by the compiler helps in eliminating a large class of bugs that arise in practice.
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.
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.