Skip to content

Functional Vilnius #11: Idris and Coq

Photo of Viaceslav Pozdniakov
Hosted By
Viaceslav P.
Functional Vilnius #11: Idris and Coq

Details

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!

Photo of Functional Vilnius group
Functional Vilnius
See more events
Wix New Vilnius office
Didžioji st. 28 · Vilnius