## Webpage:

## Time:

## Venue:

- D-405 (D-Block Seminar Room)

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