Carlo Angiuli

25 papers A* 2A 2B 2Journal 17Unranked 1
YearRankTypeTitle / Venue / Authors
2026 J jnl
A dependently-typed calculus of event telicity and culminativity.
Math. Struct. Comput. Sci.
Pavel Kovalev, Carlo Angiuli
2025 J jnl
A dependently-typed calculus of event telicity and culminativity.
CoRR
Pavel Kovalev, Carlo Angiuli
2025 J jnl
Controlling unfolding in type theory.
Math. Struct. Comput. Sci.
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
2023 J jnl
An Order-Theoretic Analysis of Universe Polymorphism.
Proc. ACM Program. Lang.
Kuen-Bang Hou (Favonia), Carlo Angiuli, Reed Mullanix
2022 J jnl
A Cubical Language for Bishop Sets.
Log. Methods Comput. Sci.
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
2022 J jnl
Controlling unfolding in type theory.
CoRR
Daniel Gratzer, Jonathan Sterling, Carlo Angiuli, Thierry Coquand, Lars Birkedal
2021 — —
Computational Semantics of Cartesian Cubical Type Theory.
Carlo Angiuli
2021 J jnl
Internalizing representation independence with univalence.
Proc. ACM Program. Lang.
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner
2021 A* conf
Normalization for Cubical Type Theory.
LICS
Jonathan Sterling, Carlo Angiuli
2021 J jnl
Normalization for Cubical Type Theory.
CoRR
Jonathan Sterling, Carlo Angiuli
2021 J jnl
Syntax and models of Cartesian cubical type theory.
Math. Struct. Comput. Sci.
Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), Daniel R. Licata
2020 J jnl
A Cubical Language for Bishop Sets.
CoRR
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
2020 J jnl
Internalizing Representation Independence with Univalence.
CoRR
Carlo Angiuli, Evan Cavallo, Anders Mörtberg, Max Zeuner
2019 B conf
Cubical Syntax for Reflection-Free Extensional Equality.
FSCD
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
2019 J jnl
Cubical Syntax for Reflection-Free Extensional Equality.
CoRR
Jonathan Sterling, Carlo Angiuli, Daniel Gratzer
2018 B conf
Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities.
CSL
Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper
2018 — conf
The RedPRL Proof Assistant (Invited Paper).
LFMTP@FSCD
Carlo Angiuli, Evan Cavallo, Kuen-Bang Hou (Favonia), Robert Harper, Jonathan Sterling
2017 J jnl
Computational Higher Type Theory III: Univalent Universes and Exact Equality.
CoRR
Carlo Angiuli, Kuen-Bang Hou (Favonia), Robert Harper
2017 A* conf
Computational higher-dimensional type theory.
POPL
Carlo Angiuli, Robert Harper, Todd Wilson
2016 A conf
Automatically Splitting a Two-Stage Lambda Calculus.
ESOP
Nicolas Feltman, Carlo Angiuli, Umut A. Acar, Kayvon Fatahalian
2016 J jnl
Computational Higher Type Theory I: Abstract Cubical Realizability.
CoRR
Carlo Angiuli, Robert Harper, Todd Wilson
2016 J jnl
Computational Higher Type Theory II: Dependent Cubical Realizability.
CoRR
Carlo Angiuli, Robert Harper
2016 J jnl
Homotopical patch theory.
J. Funct. Program.
Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper
2014 A conf
Homotopical patch theory.
ICFP
Carlo Angiuli, Edward Morehouse, Daniel R. Licata, Robert Harper
2011 J jnl
The number of extremal components of a rigid measure.
J. Comb. Theory A
Carlo Angiuli, Hari Bercovici