Monthly Archives: August 2012

First steps with Agda: provable factoring

In my last post we looked at the problem of factoring an integer. We ran into an issue with the termination checker and resolved it by wrapping the recursion into a separate inductive data-type that made it explicit. The idiom … Continue reading

Posted in Computers | Tagged , , | Leave a comment

First steps with Agda: well founded recursion

Last week I finally got time to explore Agda in some detail; something I had on my list for a while. Agda is a dependently typed programming language. That means in Agda you can have a function of the type … Continue reading

Posted in Computers | Tagged | Leave a comment

Movies to make you think, part II

Some less famous movies which I found nice (in no particular order): Waltz With Bashir Annie Hall (maybe not so exotic) Pan’s Labyrinth Teen Kanya (get a version with subtitles if you don’t speak bangla) (edit: to clarify, I’m talking … Continue reading

Posted in Rest | 4 Comments