###
Idris
In Idris, types become more than just annotations – they become a powerful tool for expressing intricate relationships and ensuring program correctness.
One day I will return to writing about Idris and update my knowledge to Idris2.
2016-09
Talk
Put a Type On It: Idris Types as Propositions
Note from a talk I gave at Strangeloop showing how Curry-Howard can be applied to structuring types to represent logical propositions using Idris as the teaching language.