Syntax and Models of Cartesian Cubical Type Theory C Angiuli, G Brunerie, T Coquand, KB Hou, R Harper, DR Licata Mathematical Structures in Computer Science 31 (4), 424-468, 2021 | 56* | 2021 |

Normalization for cubical type theory J Sterling, C Angiuli LICS 2021 (36th Annual ACM/IEEE Symposium on Logic in Computer Science), 2021 | 52 | 2021 |

Cartesian cubical computational type theory: Constructive reasoning with paths and equalities C Angiuli, KB Hou, R Harper CSL 2018 (27th EACSL Annual Conference on Computer Science Logic), 2018 | 52 | 2018 |

Computational higher-dimensional type theory C Angiuli, R Harper, T Wilson POPL 2017 (44th ACM SIGPLAN Symposium on Principles of Programming Languages …, 2017 | 51 | 2017 |

Homotopical patch theory C Angiuli, E Morehouse, DR Licata, R Harper ICFP 2014 (19th ACM SIGPLAN International Conference on Functional …, 2014 | 41 | 2014 |

Internalizing representation independence with univalence C Angiuli, E Cavallo, A Mörtberg, M Zeuner POPL 2021 (48th ACM SIGPLAN Symposium on Principles of Programming Languages), 2021 | 34 | 2021 |

Cubical syntax for reflection-free extensional equality J Sterling, C Angiuli, D Gratzer FSCD 2019 (4th International Conference on Formal Structures for Computation …, 2019 | 29 | 2019 |

Computational semantics of Cartesian cubical type theory C Angiuli PhD thesis. Pittsburgh, PA, USA: Carnegie Mellon University, 2019 | 25 | 2019 |

Computational higher type theory I: Abstract cubical realizability C Angiuli, R Harper, T Wilson arXiv preprint arXiv:1604.08873, 2016 | 24 | 2016 |

The RedPRL proof assistant C Angiuli, E Cavallo, KB Hou, R Harper, J Sterling LFMTP 2018 (13th International Workshop on Logical Frameworks and Meta …, 2018 | 21* | 2018 |

A cubical language for Bishop sets J Sterling, C Angiuli, D Gratzer Logical Methods in Computer Science 18 (1), 2022 | 17 | 2022 |

Computational higher type theory II: Dependent cubical realizability C Angiuli, R Harper arXiv preprint arXiv:1606.09638, 2016 | 17 | 2016 |

Computational higher type theory III: Univalent universes and exact equality C Angiuli, KB Hou, R Harper arXiv preprint arXiv:1712.01800, 2017 | 16* | 2017 |

Homotopical patch theory C Angiuli, E Morehouse, DR Licata, R Harper Journal of Functional Programming 26, e18, 2016 | 13 | 2016 |

Meaning explanations at higher dimension C Angiuli, R Harper Indagationes Mathematicae 29 (1), 135-149, 2018 | 11 | 2018 |

Automatically splitting a two-stage lambda calculus N Feltman, C Angiuli, UA Acar, K Fatahalian ESOP 2016 (25th European Symposium on Programming), 255-281, 2016 | 11 | 2016 |

Controlling unfolding in type theory D Gratzer, J Sterling, C Angiuli, T Coquand, L Birkedal arXiv preprint arXiv:2210.05420, 2022 | 6 | 2022 |

and Robert Harper C Angiuli, KB Hou Computational higher type theory III: Univalent universes and exact equality, 2017 | 5 | 2017 |

An Order-Theoretic Analysis of Universe Polymorphism KB Hou, C Angiuli, R Mullanix POPL 2023 (50th ACM SIGPLAN Symposium on Principles of Programming Languages), 2023 | 4 | 2023 |

Gluing models of type theory along flat functors J Sterling, C Angiuli Unpublished manuscript, 2020 | 4 | 2020 |