Research

Broadly speaking, I am interested in type theories and their applications in programming languages. In the past, I worked on supporting the verification of lambda-encoded programs in a type system and in a higher-order logic. I also enjoyed working on Haskell-style type class, which leads to a connection to term rewriting. I was excited to discover that we can verify and program with nested data types in a total programming language with dependent types. Recently, I am working on the design and implementation of a linear dependently typed programming language for circuit design.

Education


Papers


Projects


Teaching


Talks


Notes