About Logic - Dependent Types
I wrote the blog post yesterday, before I saw this. See Thorsten Altenkirch on NaÏve Type Theory and An Interesting and Useful Duality . 19:09 He mentioned Conor McBride talking about dependent type theory as a revolution. I found this series of 8 talks he did at Cambridge in 2013: Dependently Typed Metaprogramming . The course notes are available here : If you have never met a metaprogram in a dependently typed programming language like Agda [Norell, 2008], then prepare to be underwhelmed. Once we have types which can depend computationally upon first class values, metaprograms just become ordinary programs manipulating and interpreting data which happen to stand for types and operations. See also Jesper Cockx - Elaborating Dependent (Co)pattern Matching . Subscribe to About Logic .