Carlo Angiuli

According to our database, Carlo Angiuli authored at least 16 papers between 2016 and 2023.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2023

An Order-Theoretic Analysis of Universe Polymorphism.

Kuen-Bang Hou (Favonia), Carlo Angiuli, Reed Mullanix

Proc. ACM Program. Lang., January, 2023

2022

A Cubical Language for Bishop Sets.

Jonathan Sterling, Carlo Angiuli, Daniel Gratzer

Log. Methods Comput. Sci., 2022

Controlling unfolding in type theory.

Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal

CoRR, 2022

2021

Computational Semantics of Cartesian Cubical Type Theory.

Carlo Angiuli

PhD thesis, 2021

Internalizing representation independence with univalence.

Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner

Proc. ACM Program. Lang., 2021

Syntax and models of Cartesian cubical type theory.

Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata

Math. Struct. Comput. Sci., 2021

Normalization for Cubical Type Theory.

Jonathan Sterling, Carlo Angiuli

Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science, 2021

2019

Cubical Syntax for Reflection-Free Extensional Equality.

Jonathan Sterling, Carlo Angiuli, Daniel Gratzer

Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction, 2019

2018

The RedPRL Proof Assistant (Invited Paper).

Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper, Jonathan Sterling

Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2018

Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities.

Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper

Proceedings of the 27th EACSL Annual Conference on Computer Science Logic, 2018

2017

Computational Higher Type Theory III: Univalent Universes and Exact Equality.

Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper

CoRR, 2017

Computational higher-dimensional type theory.

Carlo Angiuli, Robert Harper, Todd Wilson

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016

Homotopical patch theory.

Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper

J. Funct. Program., 2016

Computational Higher Type Theory II: Dependent Cubical Realizability.

Carlo Angiuli, Robert Harper

CoRR, 2016

Computational Higher Type Theory I: Abstract Cubical Realizability.

Carlo Angiuli, Robert Harper, Todd Wilson

CoRR, 2016

Automatically Splitting a Two-Stage Lambda Calculus.

Nicolas Feltman, Carlo Angiuli, Umut A. Acar, Kayvon Fatahalian

Proceedings of the Programming Languages and Systems, 2016