In this videos, we walk through two examples to see how the programming language Idris can be used to prove theorems. The codes shown in this video were all written using Idris 2.
The slides about Twelf can be found at: https://homepages.dcc.ufmg.br/~fernan...
There are also four videos:
Part 1: • Twelf - Part 1
Part 2: • Twelf - Part 2
Part 3: • Twelf - Part 3
Part 4: • Twelf - Part 4
Idris 2 documentation: https://idris2.readthedocs.io/