It was recently announced that we got the best paper award at GPCE 2018 for our paper on Verification of High-Level Transformations with Inductive Refinement Types. The paper is about how we build a sound and efficient static analyzer for a large subset of Rascal based on Schmidt-style...
The first ever conference on Probabilstic Programming (PROBPROG 2018) was recently held at MIT. If you don’t know it, probabilistic programming is an exciting new field, that augments traditional programming languages with constructs from probability theory, including random variables, distributions and conditioning. I genuinly believe that probabilistic programming is...
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.