I am currently an engineer at Draper Labs in Cambridge. My interests include software verification and language design, logic and computability, proof theory and other things.
9 $\lambda$-calculus with reflection jul 12 '12
7 Why are dependently typed languages such as Agda used for proofs, if supercompilers for simpler typed languages can do the same? may 21 '14
7 Approximating the Kolmogorov complexity sep 13 '12
7 Inferring refinement types aug 1 '12
7 Sorting algorithms which accept a random comparator jun 12 '12