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.
21 Formal program verification in practice Aug 20 '13
15 $\lambda$-calculus with reflection Jul 12 '12
9 Why are dependently typed languages such as Agda used for proofs, if supercompilers for simpler typed languages can do the same? May 21 '14
9 Inferring refinement types Aug 1 '12
9 Sorting algorithms which accept a random comparator Jun 12 '12
8 Approximating the Kolmogorov complexity Sep 13 '12