https://orcid.org/0000-0002-0585-5564I am a postdoctoral fellow at Aarhus University in the Logic and Semantics group supervised by L. Birkedal; I am currently finishing my PhD at Carnegie Mellon University under R. Harper. I study programming languages and semantics using type theory, category theory, and topos theory as a guide. Previously I received a B.A. in Linguistics from U.C. Berkeley. My other interests include category theory, topos theory, formalization of mathematics, Assyriology, and ancient languages and literature. Research Blog Bibliography Curriculum Vitae
Research
Central to both the design of programming languages and the practice of software engineering is the tension between abstraction and composition. I employ semantic methods to design, verify, and implement languages and tools that enable both programmers and mathematicians to negotiate the different levels of abstraction that arise in their work. I apply my research to security qua information flow control, interactive theorem provers, global safety properties of programming languages, and higher-dimensional mathematics (homotopy theory).
My most recent and significant result is the proof of normalization and decidability of definitional equality for cubical type theory, a computational version of Homotopy Type Theory. My colleagues and I have also developed the redtt and cooltt proof assistants for Cartesian cubical type theory.
Recent News
| Oct. '21 | awarded PhD by Carnegie Mellon University |
| Sep. '21 | successfully defended my dissertation, moved to Aarhus |
| Jun. '21 | accepted postdoctoral position working with L. Birkedal |
| Aug. '20 | thesis proposal presented and accepted |
| Jul. '19 | received ICFP '19 Distinguished Paper Award |
| Jun. '19 | received FSCD '19 Best Paper Award for Junior Researchers |
Doctoral Dissertation
| Sep. '21 | Carnegie Mellon University |
Recent Drafts
| Dec. '20 | PreprintSyntactic categories for dependent type theory: sketching and adequacy |
| Feb. '20 | PreprintA Cubical Language for Bishop Sets |
Publications
| Jul. '21 | 49th ACM SIGPLAN Symposium on Principles of Programming Languages |
| JFP | Journal of Functional Programming, Bob Harper Festschrift Collection |
| LICS '21 | 36th Annual Symposium on Logic in Computer Science |
| JACM | Journal of the ACM |
| ICFP '19 | International Conference on Functional Programming (ICFP), 2019 ICFP '19 Distinguished Paper Award |
| FSCD '19 | International Conference on Formal Structures for Computation and Deduction (FSCD), 2019 FSCD '19 Best Paper Award for Junior Researchers |
| LFMTP '18 | International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018 |
| LICS '18 | Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '18) |
| LEUS | In: Redmond J., Pombo Martins O., Nepomuceno Fernández Á. (eds) Epistemology, Knowledge and the Impact of Interaction. Logic, Epistemology, and the Unity of Science, vol 38. Springer, Cham. |
Funding and Grants
| AFOSR | Session Types and Phase Distinctions for Noninterference (2021) Unfunded Collaborator Air Force Office of Scientific Research FA9550-21-1-0385 |
Academic Service
I have served as an external reviewer or subreviewer for CSL (2021, 2022), ESOP (2021), FSCD (2019, 2020), FoSSaCS (2021), LICS (2017, 2021); and as a referee for LMCS and MSCS.
Workshop Talks
| CT20→21 | Normalization for cubical type theory |
| ML '21 | A metalanguage for multi-phase modularity |
| HoTT '19 | Cubical Exact Equality and Categorical Gluing International Conference on Homotopy Type Theory, 2019 |
| TYPES '19 | XTT: Cubical Syntax for Extensional Equality (without equality reflection) TYPES 2019 |
Other Talks
| Oct. '21 | Normalization for (Cartesian) Cubical Type Theory MURI Team Meeting 2021 |
| Aug. '21 | Abstraction, composition, and the phase distinction CMU Speakers Club |
| May '21 | Normalization for Cubical Type Theory Padova Logic Seminar |
| Apr. '21 | Logical Relations As Types |
| Feb. '21 | Normalization for Cubical Type theory |
| Aug. '20 | Objective Metatheory of (Cubical) Type Theories Thesis Proposal |
| Jun. '20 | redtt and the future of Cartesian cubical type theory |
| Mar. '20 | Objective Metatheory of Dependent Type Theories |
| Mar. '20 | (Cubical) Computability Structures MURI Team Meeting 2020 |
| Jan. '20 | Gluing Models of Type Theory Along Flat Functors CMU HoTT Seminar |
| Apr. '19 | Algebraic Type Theory and the Gluing Construction CMU HoTT Seminar |
| Aug. '18 | redtt: implementing cartesian cubical type theory Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory |
Teaching
| Fall 2018 | TA for Constructive Logic (15-317) with Karl Crary |
| Fall 2017 | TA for Constructive Logic (15-317) with Frank Pfenning |
Awards
| 2019 | ICFP '19 Distinguished Paper Award |
| 2019 | FSCD '19 Best Paper Award for Junior Researchers |
| 2011 | W.K. Pritchett Prize in Elementary Greek, UC Berkeley |
Other Activities
Together with my co-hosts David Christiansen and Darin Morrison, I helped create The Type Theory Podcast.