Introducing the programming language Cubical Agda implementing univalent cubical homotopy type theory with higher inductive types:
On cubical homotopy type theory implemented in the proof assistant Cubical Agda:
Guarded Cubical Type Theory: Path Equality for Guarded Recursion, Lars Birkedal, Ale? Bizjak?, Ranald Clouston?, Hans Bugge Grathwohl?, Bas Spitters, Andrea Vezzosi, (arXiv:1606.05223)
Magnus Baunsgaard Kristensen?, Rasmus Ejlers Møgelberg, Andrea Vezzosi, Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks (arXiv:2102.01969)
Last revised on December 26, 2022 at 22:57:00. See the history of this page for a list of all contributions to it.