HTTP/2 200 server: GitHub.com content-type: text/html; charset=utf-8 last-modified: Thu, 06 May 2021 20:43:17 GMT access-control-allow-origin: * etag: W/"609454e5-481" expires: Tue, 30 Dec 2025 03:56:11 GMT cache-control: max-age=600 content-encoding: gzip x-proxy-cache: MISS x-github-request-id: A1ED:3ABDEF:97D71E:AAB81F:69534B03 accept-ranges: bytes age: 0 date: Tue, 30 Dec 2025 03:46:11 GMT via: 1.1 varnish x-served-by: cache-bom-vanm7210087-BOM x-cache: MISS x-cache-hits: 0 x-timer: S1767066371.021610,VS0,VE259 vary: Accept-Encoding x-fastly-request-id: f0fb4c31a96790e3a530dbe544bb26a4647fd6ff content-length: 624

Jasper Hugunin

About Me

You can contact me by email at jhugunin@cs.cmu.edu. My ORCID is 0000-0002-1133-5354. My resume (somewhat out of date) is here.

Drafts

• Constructing Inductive-Inductive Types in Cubical Type Theory. Published in FoSSaCS 2019. pdf
• Why Not W?. Accepted to TYPES 2020 post-proceedings. pdf

Talks

• 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).