Susan Potter

Idris :: Full dependent types and more!

talks

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.