A simple way to show Turing-completeness of a particular language is by encoding a Turing-equivalent computation system in it. Here we show Turing-completness of Agda, by encoding the Cyclic Tag System in it.

The Boolean Blindness blog post by Dr. Robert Harper presents a generally excellent point: the use of Booleans is inherently connected with a loss of information, the so-called Boolean Blindness. For example, even if we for some list xs know that the expression all even xs = True holds, we often can not use that information further along in our program1 and we still have to handle the cases where an element is odd, even though such case is impossible in practice.

If you are interested to know more about me, please visit About. Research and Projects will tell you more about the interesting things I had worked on before and am working on now. Otherwise, stay tuned for there is more to come.