Home

Welcome

Welcome to my blog!

Types give us a notion of possible values and dependent-type theory blurs the distinction between type and value. The symbols Π and Σ are the more distinguishing type-formers in dependent-type theory, hence the home-page welcome pictures. This blog assumes familiarity with the Agda programming language.

I've reproduced a list of recent posts here for your reading pleasure:

Posts

• SoP3: Guarded Commands - April 16, 2016
• SoP2: Interpreted Function Symbols - April 2, 2016
• SoP1: Assignment - March 31, 2016
• The Science of Programming : Why be correct? - March 28, 2016
• Graphs are to categories as lists are to monoids - March 27, 2016
• Why dependent types - January 16, 2016
• Blogging Literately: markdown from literate agda - January 12, 2016
• The making of a blog using Hakyll, Disqus, and Bitbucket - January 12, 2015

…or you can find more in the archives.