Follow
Carlo Angiuli
Carlo Angiuli
Assistant Professor, Indiana University
Verified email at indiana.edu - Homepage
Title
Cited by
Cited by
Year
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
55*2021
Normalization for cubical type theory
J Sterling, C Angiuli
LICS 2021 (36th Annual ACM/IEEE Symposium on Logic in Computer Science), 2021
522021
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
522018
Computational higher-dimensional type theory
C Angiuli, R Harper, T Wilson
POPL 2017 (44th ACM SIGPLAN Symposium on Principles of Programming Languages …, 2017
512017
Homotopical patch theory
C Angiuli, E Morehouse, DR Licata, R Harper
ICFP 2014 (19th ACM SIGPLAN International Conference on Functional …, 2014
412014
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
332021
Cubical syntax for reflection-free extensional equality
J Sterling, C Angiuli, D Gratzer
FSCD 2019 (4th International Conference on Formal Structures for Computation …, 2019
292019
Computational semantics of Cartesian cubical type theory
C Angiuli
PhD thesis. Pittsburgh, PA, USA: Carnegie Mellon University, 2019
252019
Computational higher type theory I: Abstract cubical realizability
C Angiuli, R Harper, T Wilson
arXiv preprint arXiv:1604.08873, 2016
242016
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
172022
Computational higher type theory II: Dependent cubical realizability
C Angiuli, R Harper
arXiv preprint arXiv:1606.09638, 2016
172016
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
132016
Meaning explanations at higher dimension
C Angiuli, R Harper
Indagationes Mathematicae 29 (1), 135-149, 2018
112018
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
112016
Controlling unfolding in type theory
D Gratzer, J Sterling, C Angiuli, T Coquand, L Birkedal
arXiv preprint arXiv:2210.05420, 2022
62022
and Robert Harper
C Angiuli, KB Hou
Computational higher type theory III: Univalent universes and exact equality, 2017
52017
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
42023
Gluing models of type theory along flat functors
J Sterling, C Angiuli
Unpublished manuscript, 2020
42020
The system can't perform the operation now. Try again later.
Articles 1–20