Tata Institute of Fundamental Research
Interactive Theorem Proving in Coq and the Curry-Howard Isomorphism
Project Seminar
Speaker:
Abhishek Singh
Date:
Friday, 20 Feb 2015, 11:00 to 12:30
Venue:
D-405 (D-Block Seminar Room)
(Scan to add to calendar)
Abstract:
Abstract: There seems to be a general consensus among mathematicians about the notion of a correct proof. Still, in mathematical literature, many invalid proofs remain accepted over a long period of time. It happens mostly because proofs are incomplete, and it is easy to make mistake while verifying an incomplete proof. However, writing a complete proof on paper consumes a lot of time and effort. Proof Assistants, such as Coq, can minimize these overheads. It provides the user with lots of tools and tactics to interactively develop a proof. Realization of such a computer based tool for representing proofs and propositions, is made possible because of the Curry-Howard Isomorphism. It tells us that, proving and programming are essentially equivalent tasks. More precisely, we can use a programming paradigm such as typed lambda calculus to encode propositions and their proofs. In this talk we will see, how Curry-Howard Isomorphism makes it possible to encode different logics in the Coq Proof Assistant.
| Speaker: | Abhishek Singh |
| Date: | Friday, 20 Feb 2015, 11:00 to 12:30 |
| Venue: | D-405 (D-Block Seminar Room) |
(Scan to add to calendar)
Abstract:
Abstract: There seems to be a general consensus among mathematicians about the notion of a correct proof. Still, in mathematical literature, many invalid proofs remain accepted over a long period of time. It happens mostly because proofs are incomplete, and it is easy to make mistake while verifying an incomplete proof. However, writing a complete proof on paper consumes a lot of time and effort. Proof Assistants, such as Coq, can minimize these overheads. It provides the user with lots of tools and tactics to interactively develop a proof. Realization of such a computer based tool for representing proofs and propositions, is made possible because of the Curry-Howard Isomorphism. It tells us that, proving and programming are essentially equivalent tasks. More precisely, we can use a programming paradigm such as typed lambda calculus to encode propositions and their proofs. In this talk we will see, how Curry-Howard Isomorphism makes it possible to encode different logics in the Coq Proof Assistant.