Functional Vilnius #11: Idris and Coq

Hosted By
Viaceslav P.

Details
It is normal to doubt if n - 1 + 1 = n.
-
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. -
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!

Functional Vilnius
See more events
Wix New Vilnius office
Didžioji st. 28 · Vilnius
Functional Vilnius #11: Idris and Coq