Andrea Vezzosi, Anders Mörtberg, Andreas Abel 0001
Cubical agda: a dependently typed programming language with univalence and higher inductive types
ICFP, 2019.
@article{ICFP-2019-VezzosiM0,
author = "Andrea Vezzosi and Anders Mörtberg and Andreas Abel 0001",
doi = "10.1145/3341691",
journal = "{Proceedings of the ACM on Programming Languages}",
number = "ICFP",
pages = "29",
title = "{Cubical agda: a dependently typed programming language with univalence and higher inductive types}",
volume = 3,
year = 2019,
}
Tags: