, 952-686-3386

Danny Gratzer


I'm an undergraduate student at CMU fascinated by types and programming languages. I'm particularly interested in using modern programming language research and functional languages to tackle real and significant problems. I love type theory, math, and juggling.


  • BS in Computer Science at Carnegie Mellon (2014 -)
  • PSEO at the University of Minnesota (2012 - 2014)
  • High School at Edina High School (2010 - 2014)


  • Research Assistant at Carnegie Mellon (Sept. 2014 -)

    I am currently working under Karl Crary in programming languages and type theory.

  • Camp Counselor at The Works Science Museum (June 2014 - August 2014)

    I taught elementary school children to program using Python and Minecraft. I ended up rewriting a lot of the curriculum and instruction materials for future camps and instructors.

  • Summer Intern at CSAIL at MIT (May 2013 - Sept. 2013)

    I worked Adam Chlipala building and verifying a compiler for a simple functional language to a variant of C. I both built and verified this compiler using Coq. This was part of the Bedrock project which aims to provide a full platform from assembly up amenable to formal verification.

  • Research Assistant at the University of Minnesota (Sept. 2013 - May 2013)

    I worked under John Riedl and Michael Ekstrand on Lenskit, a hotbed for building and testing recommendation algorithms. I integrated the set of algorithms built for GraphChi with Lenskit in lenskit-graphchi as well as making several changes to Lenskit proper.

Open Source

I have a lot of open source projects. Most of these can be found at and Some highlights include

  • hasquito - a compiler for a lazy functional language
  • c_of_scheme - a compiler for Scheme
  • hlf - an implemention of a Twelf-like dependently typed language
  • ds-kanren - a DSL for mini-Kanren in Haskell

Additionally, I run a blog about Haskell and programming languages at


I'm very experienced with a number of functional languages including Haskell, SML, Coq, Agda and Scheme. Additionally, I'm familiar with C, Python, and Java.