Bibliography of Cubical Type Theory

@article{swan-uemura:2022,
  author = {Swan, Andrew W. and Uemura, Taichi},
  publisher = {Cambridge University Press},
  year = {2022},
  doi = {10.1017/S0960129522000068},
  journal = {Mathematical Structures in Computer Science},
  pages = {1--20},
  title = {On Church's thesis in cubical assemblies},
}

@article{bentzen:2022,
  author = {Bentzen, Bruno},
  publisher = {Cambridge University Press},
  year = {2022},
  doi = {10.1017/S096012952200007X},
  journal = {Mathematical Structures in Computer Science},
  pages = {1--27},
  title = {Naive cubical type theory},
}

@article{sterling-angiuli-gratzer:2022,
  author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
  year = {2022},
  month = mar,
  doi = {10.46298/lmcs-18(1:43)2022},
  eprint = {2003.01491},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  issue = {1},
  journal = {Logical Methods in Computer Science},
  title = {{A Cubical Language for Bishop Sets}},
  volume = {18},
}

@article{coquand-huber-sattler:2022,
  author = {Coquand, Thierry and Huber, Simon and Sattler, Christian},
  url = {https://lmcs.episciences.org/9043},
  year = {2022},
  month = feb,
  doi = {10.46298/lmcs-18(1:28)2022},
  issue = {1},
  journal = {Logical Methods in Computer Science},
  title = {{Canonicity and homotopy canonicity for cubical type theory}},
  volume = {18},
}

@inproceedings{brunerie-ljungstrom-mortberg:2022,
  author = {Brunerie, Guillaume and Ljungstr\"{o}m, Axel and M\"{o}rtberg, Anders},
  editor = {Manea, Florin and Simpson, Alex},
  address = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f\"{u}r Informatik},
  booktitle = {30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  year = {2022},
  isbn = {978-3-95977-218-1},
  issn = {1868-8969},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{Synthetic Cohomology Theory in Cubical Agda}},
  volume = {216},
}

@article{mortberg:2021,
  author = {M\"{o}rtberg, Anders},
  publisher = {Cambridge University Press},
  year = {2021},
  doi = {10.1017/S0960129521000311},
  journal = {Mathematical Structures in Computer Science},
  pages = {1--38},
  title = {Cubical methods in homotopy type theory and univalent foundations},
}

@article{kidney-wu:2021,
  author = {Kidney, Donnacha Ois\'{i}n and Wu, Nicolas},
  address = {New York, NY, USA},
  publisher = {Association for Computing Machinery},
  year = {2021},
  month = aug,
  doi = {10.1145/3473577},
  journal = {Proceedings of the ACM on Programming Languages},
  keywords = {graph search,Haskell,Agda,monad},
  number = {ICFP},
  title = {Algebras for Weighted Search},
  volume = {5},
}

@article{abchfl:2021,
  author = {Angiuli, Carlo and Brunerie, Guillaume and Coquand, Thierry and Harper, Robert and {Hou (Favonia)}, Kuen-Bang and Licata, Daniel R.},
  publisher = {Cambridge University Press},
  year = {2021},
  doi = {10.1017/S0960129521000347},
  journal = {Mathematical Structures in Computer Science},
  number = {4},
  pages = {424--468},
  title = {Syntax and models of {C}artesian cubical type theory},
  volume = {31},
}

@article{acmz:2021,
  author = {Angiuli, Carlo and Cavallo, Evan and M\"{o}rtberg, Anders and Zeuner, Max},
  address = {New York, NY, USA},
  publisher = {Association for Computing Machinery},
  year = {2021},
  month = jan,
  doi = {10.1145/3434293},
  journal = {Proceedings of the ACM on Programming Languages},
  keywords = {Proof Assistants,Higher Inductive Types,Cubical Type Theory,Univalence,Representation Independence},
  number = {POPL},
  pages = {1--30},
  title = {Internalizing Representation Independence with Univalence},
  volume = {5},
}

@inproceedings{forsberg-xu-ghani:2020,
  author = {Forsberg, Fredrik Nordvall and Xu, Chuangjie and Ghani, Neil},
  address = {New Orleans, LA, USA},
  publisher = {Association for Computing Machinery},
  booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  year = {2020},
  doi = {10.1145/3372885.3373835},
  isbn = {978-1-4503-7097-4},
  keywords = {higher inductive types,Ordinal notation,cubical Agda,Cantor normal form,inductive-inductive definitions},
  pages = {172--185},
  title = {Three Equivalent Ordinal Notation Systems in {Cubical Agda}},
}

@inproceedings{cavallo-harper:2020,
  author = {Cavallo, Evan and Harper, Robert},
  editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
  address = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  url = {https://drops.dagstuhl.de/opus/volltexte/2020/11656},
  annotation = {Keywords: parametricity, cubical type theory, higher inductive types},
  booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  year = {2020},
  doi = {10.4230/LIPIcs.CSL.2020.13},
  isbn = {978-3-95977-132-0},
  issn = {1868-8969},
  pages = {13:1--13:17},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{Internal Parametricity for Cubical Type Theory}},
  volume = {152},
}

@inproceedings{mortberg-pujet:2020,
  author = {M\"{o}rtberg, Anders and Pujet, Lo\"{i}c},
  address = {New Orleans, LA, USA},
  publisher = {Association for Computing Machinery},
  booktitle = {Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs},
  year = {2020},
  doi = {10.1145/3372885.3373825},
  isbn = {978-1-4503-7097-4},
  keywords = {Constructive Mathematics,Cubical Type Theory,Homotopy Type Theory,Synthetic Homotopy Theory},
  pages = {158--171},
  title = {{Cubical Synthetic Homotopy Theory}},
}

@inproceedings{cavallo-mortberg-swan:2020,
  author = {Cavallo, Evan and M\"{o}rtberg, Anders and Swan, Andrew W},
  editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca},
  address = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  url = {https://drops.dagstuhl.de/opus/volltexte/2020/11657},
  booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  year = {2020},
  doi = {10.4230/LIPIcs.CSL.2020.14},
  isbn = {978-3-95977-132-0},
  issn = {1868-8969},
  pages = {14:1--14:17},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{Unifying Cubical Models of Univalent Type Theory}},
  volume = {152},
}

@article{bch:2019,
  author = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
  date = {2019-08-01},
  doi = {10.1007/s10817-018-9472-6},
  journaltitle = {Journal of Automated Reasoning},
  number = {2},
  pages = {159--171},
  title = {The Univalence Axiom in Cubical Sets},
  volume = {63},
}

@article{cavallo-harper:2019,
  author = {Cavallo, Evan and Harper, Robert},
  address = {New York, NY, USA},
  publisher = acm,
  year = {2019},
  month = jan,
  doi = {10.1145/3290314},
  issn = {2475-1421},
  journal = {Proceedings of the ACM on Programming Languages},
  keywords = {cubical type theory,higher inductive types,homotopy type theory},
  number = {POPL},
  pages = {1:1--1:27},
  title = {Higher Inductive Types in Cubical Computational Type Theory},
  volume = {3},
}

@inproceedings{vezzosi-mortberg-abel:2019,
  author = {Vezzosi, Andrea and M\"{o}rtberg, Anders and Abel, Andreas},
  address = {Boston, Massachusetts, USA},
  publisher = {Association for Computing Machinery},
  booktitle = {Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming},
  year = {2019},
  doi = {10.1145/3341691},
  title = {{Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types}},
}

@inproceedings{sterling-angiuli-gratzer:2019,
  author = {Sterling, Jonathan and Angiuli, Carlo and Gratzer, Daniel},
  editor = {Geuvers, Herman},
  location = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  url = {http://drops.dagstuhl.de/opus/volltexte/2019/10538},
  booktitle = {Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  date = {2019},
  doi = {10.4230/LIPIcs.FSCD.2019.31},
  eprint = {1904.08562},
  eprinttype = {arXiv},
  isbn = {978-3-95977-107-8},
  issn = {1868-8969},
  pages = {31:1--31:25},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {Cubical Syntax for Reflection-Free Extensional Equality},
  volume = {131},
}

@article{huber:2018,
  author = {Huber, Simon},
  year = {2018},
  month = jun,
  doi = {10.1007/s10817-018-9469-1},
  issn = {1573-0670},
  journal = {Journal of Automated Reasoning},
  title = {Canonicity for Cubical Type Theory},
}

@inproceedings{coquand-huber-mortberg:2018,
  author = {Coquand, Thierry and Huber, Simon and M\"{o}rtberg, Anders},
  address = {Oxford, United Kingdom},
  publisher = acm,
  booktitle = {Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science},
  year = {2018},
  doi = {10.1145/3209108.3209197},
  isbn = {978-1-4503-5583-4},
  pages = {255--264},
  title = {On Higher Inductive Types in Cubical Type Theory},
}

@inproceedings{lops:2018,
  author = {Licata, Daniel R. and Orton, Ian and Pitts, Andrew M. and Spitters, Bas},
  booktitle = {3rd International Conference on Formal Structures for Computation and Deduction, {FSCD} 2018, July 9-12, 2018, Oxford, {UK}},
  year = {2018},
  doi = {10.4230/LIPIcs.FSCD.2018.22},
  pages = {22:1--22:17},
  title = {Internal Universes in Models of Homotopy Type Theory},
}

@article{awodey:2018,
  author = {Awodey, Steve},
  year = {2018},
  doi = {10.1016/j.apal.2018.08.002},
  issn = {0168-0072},
  journal = {Annals of Pure and Applied Logic},
  keywords = {Homotopy type theory,Algebraic weak factorization system,Path object,Identity type,Martin-L\"{o}f type theory},
  note = {Logic Colloquium 2015},
  number = {12},
  pages = {1270--1294},
  title = {A cubical model of homotopy type theory},
  volume = {169},
}

@inproceedings{angiuli-favonia-harper:2018,
  author = {Angiuli, Carlo and {Hou (Favonia)}, Kuen-Bang and Harper, Robert},
  editor = {Ghica, Dan and Jung, Achim},
  address = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  url = {http://drops.dagstuhl.de/opus/volltexte/2018/9673},
  annotation = {Keywords: Homotopy Type Theory, Two-Level Type Theory, Computational Type Theory, Cubical Sets},
  booktitle = {27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  year = {2018},
  doi = {10.4230/LIPIcs.CSL.2018.6},
  isbn = {978-3-95977-088-0},
  issn = {1868-8969},
  pages = {6:1--6:17},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities}},
  volume = {119},
}

@article{cchm:2017,
  author = {Cohen, Cyril and Coquand, Thierry and Huber, Simon and M\"{o}rtberg, Anders},
  year = {2017},
  month = nov,
  eprint = {1611.02108},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  journal = {IfCoLog Journal of Logics and their Applications},
  number = {10},
  pages = {3127--3169},
  title = {{Cubical Type Theory: a constructive interpretation of the univalence axiom}},
  volume = {4},
}

@inproceedings{angiuli-harper-wilson:2017,
  author = {Angiuli, Carlo and Harper, Robert and Wilson, Todd},
  address = {Paris, France},
  publisher = {Association for Computing Machinery},
  booktitle = {POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages},
  year = {2017},
  doi = {10.1145/3009837.3009861},
  isbn = {978-1-4503-4660-3},
  keywords = {Homotopy Type Theory,Logical Relations},
  pages = {680--693},
  title = {Computational Higher-Dimensional Type Theory},
}

@inproceedings{orton-pitts:2016,
  author = {Orton, Ian and Pitts, Andrew M.},
  editor = {Talbot, Jean-Marc and Regnier, Laurent},
  address = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  booktitle = {25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  year = {2016},
  doi = {10.4230/LIPIcs.CSL.2016.24},
  isbn = {978-3-95977-022-4},
  issn = {1868-8969},
  pages = {24:1--24:19},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {Axioms for Modelling Cubical Type Theory in a Topos},
  volume = {62},
}