Bibliography of Cubical Type Theory

This page collects papers and dissertations about Cubical Type Theory; if you have written a paper or dissertation on this topic, please write to me to have it added to this list.

The following authors are represented in this bibliography: Frederik Lerbjerg Aagaard, Andreas Abel, Carlo Angiuli, Steve Awodey, Bruno Bentzen, Marc Bezem, Lars Birkedal, Aleš Bizjak, Guillaume Brunerie, Evan Cavallo, Vikraman Choudhury, Ranald Clouston, Cyril Cohen, Thierry Coquand, Marcelo Fiore, Fredrik Nordvall Forsberg, Neil Ghani, Hans Bugge Grathwohl, Daniel Gratzer, Robert Harper, Favonia, Simon Huber, Donnacha Oisín Kidney, Magnus Baunsgaard Kristensen, Daniel Licata, Axel Ljungström, Samuel Mimram, Hugo Moeneclaey, Anders Mörtberg, Rasmus Ejlers Møgelberg, Émile Oleon, Ian Orton, Andrew Pitts, Loïc Pujet, Robert Rose, Christian Sattler, Bas Spitters, Jonathan Sterling, Andrew Swan, Taichi Uemura, Niccolò Veltri, Andrea Vezzosi, Matthew Weaver, Jonathan Weinberger, Todd Wilson, Nicolas Wu, Chuangjie Xu, and Max Zeuner.

Refereed Publications

FSCD'22
To appear Division by two, in homotopy type theory
S. Mimram and É. Oleon
International Conference on Formal Structures for Computation and Deduction (FSCD)
April 2022
@inproceedings{mimram-oleon:2022,
  author = {Mimram, Samuel and \'{E}mile, Oleon},
  editor = {Felty, Amy},
  address = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  url = {http://www.lix.polytechnique.fr/Labo/Samuel.Mimram/docs/mimram_div2.pdf},
  booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)},
  year = {2022},
  month = aug,
  doi = {10.4230/LIPIcs.FSCD.2022.10},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {Division by two, in homotopy type theory},
  volume = {228},
}
MSCS
On Church's thesis in cubical assemblies
Mathematical Structures in Computer Science
March 21, 2022
@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},
}
MSCS
Naive cubical type theory
Mathematical Structures in Computer Science
March 15, 2022
@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},
}
LMCS
A Cubical Language for Bishop Sets
Logical Methods in Computer Science
February 9, 2022
@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},
}
LMCS
Canonicity and homotopy canonicity for cubical type theory
T. Coquand, S. Huber, and C. Sattler
Logical Methods in Computer Science
February 2022
@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},
}
LICS'22
Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks
M. B. Kristensen, R. E. Møgelberg, and A. Vezzosi
Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
@inproceedings{kristensen-mogelberg-vezzosi:2022,
  author = {Kristensen, Magnus Baunsgaard and M\o{}gelberg, Rasmus Ejlers and Vezzosi, Andrea},
  address = {New York, NY, USA},
  publisher = {Association for Computing Machinery},
  booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science},
  year = {2022},
  doi = {10.48550/ARXIV.2102.01969},
  title = {Greatest HITs: Higher inductive types in coinductive definitions via induction under clocks},
}
CSL'22
Synthetic Cohomology Theory in Cubical Agda
G. Brunerie, A. Ljungström, and A. Mörtberg
30th EACSL Annual Conference on Computer Science Logic (CSL 2022)
@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},
}
MSCS
Cubical methods in homotopy type theory and univalent foundations
Mathematical Structures in Computer Science
December 10, 2021
@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},
}
ICFP'21
Algebras for Weighted Search
Proceedings of the ACM on Programming Languages (ICFP)
August 2021
@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},
}
LICS '21
Normalization for Cubical Type theory
36th Annual Symposium on Logic in Computer Science
July 7, 2021
@inproceedings{sterling-angiuli:2021,
  author = {Sterling, Jonathan and Angiuli, Carlo},
  address = {Los Alamitos, CA, USA},
  publisher = {IEEE Computer Society},
  booktitle = {2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)},
  year = {2021},
  month = jul,
  doi = {10.1109/LICS52264.2021.9470719},
  eprint = {2101.11479},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  pages = {1--15},
  title = {Normalization for Cubical Type Theory},
}
MSCS
Syntax and Models of Cartesian Cubical Type Theory
Mathematical Structures in Computer Science
@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},
}
POPL'21
Internalizing Representation Independence with Univalence
Proceedings of the ACM on Programming Languages (POPL)
January 2021
@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},
}
MFPS'21
Two Guarded Recursive Powerdomains for Applicative Simulation
Proceedings 37th Conference on Mathematical Foundations of Programming Semantics
@inproceedings{mogelberg-vezzosi:2021,
  author = {M{\o{}}gelberg, {Rasmus Ejlers} and Vezzosi, Andrea},
  publisher = {Electronic Proceedings in Theoretical Computer Science},
  booktitle = {Proceedings 37th Conference on Mathematical Foundations of Programming Semantics},
  date = {2021-12},
  doi = {10.4204/EPTCS.351.13},
  pages = {200--217},
  title = {Two Guarded Recursive Powerdomains for Applicative Simulation},
  volume = {351},
}
CPP'20
Cubical Synthetic Homotopy Theory
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
@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}},
}
CSL'20
Unifying Cubical Models of Univalent Type Theory
28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
@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},
}
CSL'20
Internal Parametricity for Cubical Type Theory
28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
@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},
}
CPP'20
Formalizing π-Calculus in Guarded Cubical Agda
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
@inproceedings{veltri-vezzosi:2020,
  author = {Veltri, Niccol\`{o} and Vezzosi, Andrea},
  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.3373814},
  isbn = {978-1-4503-7097-4},
  keywords = {ticked cubical type theory,denotational semantics,guarded recursion,pi-calculus},
  pages = {270--283},
  title = {Formalizing $\pi$-Calculus in {Guarded Cubical Agda}},
}
CPP'20
Three Equivalent Ordinal Notation Systems in Cubical Agda
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
@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}},
}
JAR
The Univalence Axiom in Cubical Sets
Journal of Automated Reasoning
August 1, 2019
@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},
}
ICFP'19
Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types
Proceedings of the 24th ACM SIGPLAN International Conference on Functional Programming
@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}},
}
JAR
Guarded Cubical Type Theory
Journal of Automated Reasoning
@article{bbcgsv:2019,
  author = {Birkedal, Lars and Bizjak, Ale\v{s} and Clouston, Ranald and Grathwohl, Hans Bugge and Spitters, Bas and Vezzosi, Andrea},
  year = {2019},
  doi = {10.1007/s10817-018-9471-7},
  journal = {Journal of Automated Reasoning},
  number = {2},
  pages = {211--253},
  title = {Guarded Cubical Type Theory},
  volume = {63},
}
POPL'19
Bisimulation as Path Type for Guarded Recursive Types
Proceedings of the ACM on Programming Languages (POPL)
January 2019
@article{mogelberg-veltri:2019,
  author = {M\o{}gelberg, Rasmus Ejlers and Veltri, Niccol\`{o}},
  address = {New York, NY, USA},
  publisher = acm,
  year = {2019},
  month = jan,
  doi = {10.1145/3290317},
  journal = {Proceedings of the ACM on Programming Languages},
  number = {POPL},
  title = {Bisimulation as Path Type for Guarded Recursive Types},
  volume = {3},
}
POPL'19
Higher Inductive Types in Cubical Computational Type Theory
Proceedings of the ACM on Programming Languages (POPL)
January 2019
@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},
}
FSCD '19
Cubical Syntax for Reflection-Free Extensional Equality
International Conference on Formal Structures for Computation and Deduction (FSCD)
FSCD '19 Best Paper Award for Junior Researchers
@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},
}
JAR
Canonicity for Cubical Type Theory
Journal of Automated Reasoning
June 2018
@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},
}
APAL
A cubical model of homotopy type theory
Annals of Pure and Applied Logic
@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},
}
LICS'18
On Higher Inductive Types in Cubical Type Theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
@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},
}
CSL'18
Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities
27th EACSL Annual Conference on Computer Science Logic (CSL 2018)
@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},
}
FSCD'18
Internal Universes in Models of Homotopy Type Theory
3rd International Conference on Formal Structures for Computation and Deduction
@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},
}
JLA
Cubical Type Theory: a constructive interpretation of the univalence axiom
IfCoLog Journal of Logics and their Applications
@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},
}
2017
Invited Meaning explanations at higher dimension
Indagationes Mathematicae special issue: L.E.J. Brouwer, fifty years later
@article{angiuli-harper:2017:brouwer,
  author = {Angiuli, Carlo and Harper, Robert},
  year = {2018},
  doi = {10.1016/j.indag.2017.07.010},
  issn = {0019-3577},
  journal = {Indagationes Mathematicae},
  note = {L.E.J. Brouwer, fifty years later},
  number = {1},
  pages = {135--149},
  title = {Meaning explanations at higher dimension},
  volume = {29},
}
POPL'17
Computational Higher-Dimensional Type Theory
POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
@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},
}
CSL'16
Axioms for Modelling Cubical Type Theory in a Topos
I. Orton and A. Pitts
25th EACSL Annual Conference on Computer Science Logic (CSL 2016)
@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},
}

Unpublished Manuscripts

Oct. 2021
Preprint Free Commutative Monoids in Homotopy Type Theory
October 11, 2021
@unpublished{choudhury-fiore:2021,
  author = {Choudhury, Vikraman and Fiore, Marcelo},
  publisher = {arXiv},
  year = {2021},
  doi = {10.48550/ARXIV.2110.05412},
  note = {Under submission},
  title = {Free Commutative Monoids in Homotopy Type Theory},
}
Oct. 2016
Preprint Cubical sets and the topological topos
October 17, 2016
@unpublished{spitters:2016,
  author = {Spitters, Bas},
  year = {2016},
  eprint = {1610.05270},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  note = {Unpublished manuscript},
  title = {Cubical sets and the topological topos},
}

Workshop Presentations

TYPES'22
The 4th Homotopy Group of the 3-Sphere in Cubical Agda
A. Ljungström and A. Mörtberg
28th International Conference on Types for Proofs and Programs
June 2022
@inproceedings{ljungstrom-mortberg:2022:types,
  author = {Ljungstr\"{o}m, Axel and M\"{o}rtberg, Anders},
  booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  year = {2022},
  title = {The 4th Homotopy Group of the 3-Sphere in Cubical Agda},
}
TYPES'22
Deciding the cofibration logic of cartesian cubical type theories
R. Rose, M. Weaver, and D. Licata
28th International Conference on Types for Proofs and Programs
June 2022
@inproceedings{rose-weaver-licata:2022:types,
  author = {Rose, Robert and Weaver, Matthew and Licata, Daniel},
  booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  year = {2022},
  title = {Deciding the cofibration logic of cartesian cubical type theories},
}
TYPES'22
Extending Cubical Agda with Internal Parametricity
R. Rose, M. Weaver, and D. Licata
28th International Conference on Types for Proofs and Programs
June 2022
@inproceedings{van-muylder-vezzosi-nuyts-devriese:2022:types,
  author = {{Van Muylder}, Antoine and Vezzosi, Andrea and Nuyts, Andreas and Devriese, Dominique},
  booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  year = {2022},
  title = {Extending Cubical Agda with Internal Parametricity},
}
TYPES'22
Unifying cubical and multimodal type theory
F. L. Aagaard, M. B. Kristensen, D. Gratzer, and L. Birkedal
28th International Conference on Types for Proofs and Programs
June 2022
@unpublished{akgb:2022,
  author = {Aagaard, Frederik Lerbjerg and Kristensen, Magnus Baunsgaard and Gratzer, Daniel and Birkedal, Lars},
  publisher = {arXiv},
  year = {2022},
  doi = {10.48550/ARXIV.2203.13000},
  note = {Unpublished manuscript},
  title = {Unifying cubical and multimodal type theory},
}
TYPES'22
Cubical models are cofreely parametric
28th International Conference on Types for Proofs and Programs
June 2022
@inproceedings{moeneclaey:2022:types,
  author = {Moeneclaey, Hugo},
  booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  year = {2022},
  title = {Cubical models are cofreely parametric},
}
TYPES'22
Towards a Formalization of Affine Schemes in Cubical Agda
M. Zeuner and A. Mörtberg
28th International Conference on Types for Proofs and Programs
June 2022
@inproceedings{mortberg-zeuner:2022:types,
  author = {M\"{o}rtberg, Anders and Zeuner, Max},
  booktitle = {28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  year = {2022},
  title = {Towards a Formalization of Affine Schemes in Cubical Agda},
}
TYPES'18
Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing
24th International Conference on Types for Proofs and Programs (TYPES 2018)
@inproceedings{uemura:2019:types,
  author = {Uemura, Taichi},
  editor = {Dybjer, Peter and Santo, Jos\'{e} Esp\'{i}rito and Pinto, Lu\'{i}s},
  location = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  booktitle = {24th International Conference on Types for Proofs and Programs (TYPES 2018)},
  date = {2019},
  isbn = {978-3-95977-106-1},
  issn = {1868-8969},
  pages = {7:1--7:20},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing}},
  volume = {130},
}
LFMTP '18
Invited The RedPRL Proof Assistant
International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018
@inproceedings{redprl:2018:lfmtp,
  author = {Angiuli, Carlo and Cavallo, Evan and {Hou (Favonia)}, Kuen-Bang and Harper, Robert and Sterling, Jonathan},
  editor = {Blanqui, Fr\'{e}d\'{e}ric and Reis, Giselle},
  publisher = {Open Publishing Association},
  booktitle = {Proceedings of the 13th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP@FSCD 2018, Oxford, UK, 7th July 2018.},
  date = {2018},
  doi = {10.4204/EPTCS.274.1},
  pages = {1--10},
  title = {{The \textsf{\textcolor[rgb]{.91,.31,.27}{Red}PRL} Proof Assistant (Invited Paper)}},
}
TYPES'13
A Model of Type Theory in Cubical Sets
19th International Conference on Types for Proofs and Programs (TYPES 2013)
@inproceedings{bch:2014,
  author = {Bezem, Marc and Coquand, Thierry and Huber, Simon},
  editor = {Matthes, Ralph and Schubert, Aleksy},
  address = {Dagstuhl, Germany},
  publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  url = {http://drops.dagstuhl.de/opus/volltexte/2014/4628},
  annotation = {Keywords: Models of dependent type theory, cubical sets, Univalent Foundations},
  booktitle = {19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  year = {2014},
  doi = {10.4230/LIPIcs.TYPES.2013.107},
  isbn = {978-3-939897-72-9},
  issn = {1868-8969},
  pages = {107--128},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  title = {{A Model of Type Theory in Cubical Sets}},
  volume = {26},
}

Dissertations

Apr. 2022
Dissertation Overview: First Steps in Synthetic Tait Computability
Dissertation Overview, Carnegie Mellon University
@unpublished{sterling:2022:thesis:overview,
  author = {Sterling, Jonathan},
  url = {https://www.jonmsterling.com/papers/sterling:2022:thesis:overview.pdf},
  year = {2022},
  month = apr,
  note = {Synopsis of doctoral dissertation, Carnegie Mellon University},
  title = {Dissertation Overview: \emph{First Steps in Synthetic {Tait} Computability}},
}
Sep. 2021
First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory
Doctoral Dissertation, Carnegie Mellon University
September 13, 2021
@phdthesis{sterling:2021:thesis,
  author = {Sterling, Jonathan},
  school = {Carnegie Mellon University},
  year = {2021},
  doi = {10.5281/zenodo.5709838},
  note = {CMU technical report CMU-CS-21-142},
  title = {First Steps in Synthetic {Tait} Computability: The Objective Metatheory of Cubical Type Theory},
}
Feb. 2021
Higher Inductive Types and Internal Parametricity for Cubical Type Theory
Doctoral Dissertation, Carnegie Mellon University
@phdthesis{cavallo:2021,
  author = {Cavallo, Evan},
  school = {Carnegie Mellon University},
  year = {2021},
  number = {CMU-CS-21-100},
  title = {Higher Inductive Types and Internal Parametricity for Cubical Type Theory},
}
Sep. 2020
Finiteness in cubical type theory
Masters by Research Thesis, University College Cork
@mastersthesis{kidney:2020,
  author = {Kidney, Donnacha Ois\'{i}n},
  school = {University College Cork},
  url = {https://cora.ucc.ie/handle/10468/11338},
  year = {2020},
  title = {Finiteness in cubical type theory},
}
2019
Computational Semantics of Cartesian Cubical Type Theory
Doctoral Dissertation, Carnegie Mellon University
@phdthesis{angiuli:2019,
  author = {Angiuli, Carlo},
  school = {Carnegie Mellon University},
  year = {2019},
  number = {CMU-CS-19-127},
  title = {Computational Semantics of Cartesian Cubical Type Theory},
}
Nov. 2016
The Cubical Model of Type Theory
J. Weinberger
Masters Thesis, Technische Universität Darmstadt
November 1, 2016
@mastersthesis{weinberger:2016,
  author = {Weinberger, Jonathan},
  school = {Technische Universit\"{a}t Darmstadt},
  url = {https://www2.mathematik.tu-darmstadt.de/~streicher/THESES/weinberger.pdf},
  year = {2016},
  month = nov,
  title = {The Cubical Model of Type Theory},
}
2016
Cubical Interpretations of Type Theory
Doctoral Dissertation, University of Gothenburg
@phdthesis{huber:2016,
  author = {Huber, Simon},
  school = {University of Gothenberg},
  year = {2016},
  title = {Cubical Interpretations of Type Theory},
}

Technical Reports

Jul. 2018
Computational Higher Type Theory IV: Inductive Types
July 18, 2018
@unpublished{cavallo-harper:2018,
  author = {Cavallo, Evan and Harper, Robert},
  year = {2018},
  month = jul,
  eprint = {1801.01568},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  title = {Computational Higher Type Theory {IV}: Inductive Types},
}
Dec. 2017
Computational Higher Type Theory III: Univalent Universes and Exact Equality
December 5, 2017
@unpublished{angiuli-favonia-harper:2017,
  author = {Angiuli, Carlo and {Hou (Favonia)}, Kuen-Bang and Harper, Robert},
  year = {2017},
  month = dec,
  eprint = {1712.01800},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  title = {Computational Higher Type Theory {III}: Univalent Universes and Exact Equality},
}
Apr. 2017
Computational Higher Type Theory II: Dependent Cubical Realizability
April 26, 2017
@unpublished{angiuli-harper:2017,
  author = {Angiuli, Carlo and Harper, Robert},
  year = {2017},
  month = apr,
  eprint = {1606.09638},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  title = {Computational Higher Type Theory {II}: Dependent Cubical Realizability},
}
Jun. 2016
Computational Higher Type Theory I: Abstract Cubical Realizability
June 14, 2016
@unpublished{angiuli-harper-wilson:2016,
  author = {Angiuli, Carlo and Harper, Robert and Wilson, Todd},
  year = {2016},
  month = jun,
  eprint = {1604.08873},
  eprintclass = {cs.LO},
  eprinttype = {arXiv},
  title = {Computational Higher Type Theory {I}: Abstract Cubical Realizability},
}