I am a postdoctoral fellow at Aarhus University in the Logic and Semantics group supervised by Lars Birkedal; I am currently finishing my PhD at Carnegie Mellon University under Robert 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 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 both enable 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

Sep. 2021 | successfully defended my dissertation |

Jun. 2021 | accepted postdoctoral position working with Lars Birkedal |

Aug. 2020 | thesis proposal presented and accepted |

Jul. 2019 | received ICFP '19 Distinguished Paper Award |

Jun. 2019 | received FSCD '19 Best Paper Award for Junior Researchers |

## Recent Drafts

Jul. 2021 | PreprintA cost-aware logical framework |

Dec. 2020 | PreprintSyntactic categories for dependent type theory: sketching and adequacy |

Feb. 2020 | PreprintA Cubical Language for Bishop Sets |

## Publications

JACM | To appearLogical Relations as Types: Proof-Relevant Parametricity for Program Modules Journal of the ACM |

LICS '21 | 36th Annual Symposium on Logic in Computer Science |

JFP | Journal of Functional Programming, Bob Harper Festschrift Collection |

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

Sep. 2021 | First Steps in Synthetic Tait Computability Doctoral Defense, Carnegie Mellon University |

Aug. 2021 | Abstraction, composition, and the phase distinction CMU Speakers Club |

May 2021 | Normalization for Cubical Type Theory Padova Logic Seminar |

Apr. 2021 | Logical Relations As Types |

Feb. 2021 | Normalization for Cubical Type theory |

Aug. 2020 | Objective Metatheory of (Cubical) Type Theories Thesis Proposal |

Jun. 2020 | redtt and the future of Cartesian cubical type theory |

Mar. 2020 | Objective Metatheory of Dependent Type Theories |

Mar. 2020 | (Cubical) Computability Structures MURI Grant Meeting |

Jan. 2020 | Gluing Models of Type Theory Along Flat Functors CMU HoTT Seminar |

Apr. 2019 | Algebraic Type Theory and the Gluing Construction CMU HoTT Seminar |

Aug. 2018 | 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.