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: http://talks.bfpg.org/talks/2015-03-24.agda_1.html

Part 2: http://talks.bfpg.org/talks/2015-04-14.agda_2.html

No comments: