Sunday, April 26, 2015

programming with dependent types

Now for something solidly in the "other things that you have to be a particular type of eclectic nerd to enjoy clumped under the same heading" category of this blog...

Brisbane, of all things, has a fantastic functional programming meetup group that has talks every month. Matt Brecknell gave an incredibly fun two-part lecture on programming with dependent types in Agda. And shockingly, he totally pulled off the live-coded format.

If you wanna ride the equality-is-a-type-and-other-ridiculous-notions rollercoaster, watch here:

Part 1:

Part 2:

No comments: