| Description |
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.
|