Carlo Angiuli

Publication Activity (10 Years)

Years Active: 2014-2023
Publications (10 Years): 19

Top Topics

Theoretic Analysis

Top Venues

Proc. ACM Program. Lang.

J. Funct. Program.

Math. Struct. Comput. Sci.

Publications

Kuen-Bang Hou (Favonia), Carlo Angiuli, Reed Mullanix
An Order-Theoretic Analysis of Universe Polymorphism. Proc. ACM Program. Lang. 7 (POPL) (2023)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
A Cubical Language for Bishop Sets. Log. Methods Comput. Sci. 18 (1) (2022)
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
Controlling unfolding in type theory. CoRR (2022)
Jonathan Sterling, Carlo Angiuli
Normalization for Cubical Type Theory. CoRR (2021)
Jonathan Sterling, Carlo Angiuli
Normalization for Cubical Type Theory. LICS (2021)
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata
Syntax and models of Cartesian cubical type theory. Math. Struct. Comput. Sci. 31 (4) (2021)
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner
Internalizing representation independence with univalence. Proc. ACM Program. Lang. 5 (POPL) (2021)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
A Cubical Language for Bishop Sets. CoRR (2020)
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner
Internalizing Representation Independence with Univalence. CoRR (2020)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
Cubical Syntax for Reflection-Free Extensional Equality. FSCD (2019)
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
Cubical Syntax for Reflection-Free Extensional Equality. CoRR (2019)
Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper
Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities. CSL (2018)
Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou, Robert Harper, Jonathan Sterling
The RedPRL Proof Assistant (Invited Paper). LFMTP@FSCD (2018)
Carlo Angiuli, Kuen-Bang Hou, Robert Harper
Computational Higher Type Theory III: Univalent Universes and Exact Equality. CoRR (2017)
Carlo Angiuli, Robert Harper, Todd Wilson
Computational higher-dimensional type theory. POPL (2017)
Nicolas Feltman, Carlo Angiuli, Umut A. Acar, Kayvon Fatahalian
Automatically Splitting a Two-Stage Lambda Calculus. ESOP (2016)
Carlo Angiuli, Robert Harper
Computational Higher Type Theory II: Dependent Cubical Realizability. CoRR (2016)
Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper
Homotopical patch theory. J. Funct. Program. 26 (2016)
Carlo Angiuli, Robert Harper, Todd Wilson
Computational Higher Type Theory I: Abstract Cubical Realizability. CoRR (2016)
Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper
Homotopical patch theory. ICFP (2014)