Functional Vilnius #11: Idris and Coq

It is normal to doubt if n - 1 + 1 = n.

1. Total functional programming and proving in Idris (Alex Gryzlov)
   In this talk I'll try to take you on a short tour through the dependently typed lands: what properties do they allow us to express, which ingredients are needed to make it work, and what are some of the challenges and perspectives of this approach.

2. Introduction to Coq (Viaceslav Pozdniakov)

In this talk we will discuss Coq - an interactive theorem prover, how it is related to math, logic, programming and dependent types.

See you!