About Me A researcher on functional programming working at Tohoku University. For more information, see my web page. Some Projects Hosted on GitHub An implementation technique of embedded DSLs called "Embedding by Unembedding" and its examples Sparcl: a partially-invertible programming language and its correctness proof in Agda An embedded language for invertible pretty printer