I am an undergraduate at the University of Washington studying Computer Science and Mathematics. Working with Dr. Dan Grossman and Talia Ringer, I wrote a paper on constructing inductive-inductive types in cubical type theory. I also contribute to the Coq proof assistant. Currently I am applying to graduate school, working towards a PhD in type theory.

You can contact me by email at jasper@hugunin.net. My ORCID is 0000-0002-1133-5354. My resume is here.

- Constructing Inductive-Inductive Types in Cubical Type Theory. Accepted to FoSSaCS 2019. pdf

- Inductive-Inductive types in Homotopy Type Theory. Presented to the Kashima research group at Tokyo Institute of Technology at the end of my study abroad period.
- Inductive-Inductive definitions without UIP. Presented at the 13th Theorem Proving and Provers Meeting (TPP 2017).