Cubical Agda: A Dependently Typed Programming Language With Univalence and Higher Inductive Types
Proceedings of the ACM on Programming Languages
doi 10.1145/3341691
Full Text
Open PDFAbstract
Available in full text
Date
July 26, 2019
Authors
Publisher
Association for Computing Machinery (ACM)