# Bibliography of Cubical Type Theory

### Table of contents

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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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, 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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 | 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}, } |