Guaranteed-Correct Programs using Dependent Types

Yesterday, the Functional Programming meet-up group in Gothenburg hosted a session on dependent types. Zimpler provided the pizzas.

During the talk we used Agda to play with dependent types and better understand their meaning.

Video and source code after the jump.

Video of the talk. Edited by Jean-Louis