# 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, Dominique Devriese, 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, Andreas Nuyts, Émile Oleon, Ian Orton, Andrew Pitts, Loïc Pujet, Robert Rose, Christian Sattler, Bas Spitters, Jonathan Sterling, Andrew Swan, Taichi Uemura, Antoine Van Muylder, 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) June 28, 2022 ## BibTeX citation@inproceedings{mimram-oleon:2022, author = {Mimram, Samuel and \'{E}mile, Oleon}, editor = {Felty, Amy}, address = {Dagstuhl, Germany}, publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, year = {2022}, month = aug, doi = {10.4230/LIPIcs.FSCD.2022.11}, 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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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.1145/3531130.3533359}, 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) ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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}, } |

MFPS '21 | Proceedings 37th Conference on Mathematical Foundations of Programming Semantics ## BibTeX citation@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}, } |

POPL '21 | Proceedings of the ACM on Programming Languages (POPL) January 2021 ## BibTeX citation@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}, } |

CPP '20 | Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs ## BibTeX citation@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}}, } |

CSL '20 | 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) ## BibTeX citation@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}, } |

CPP '20 | Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs ## BibTeX citation@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}}, } |

CSL '20 | 28th EACSL Annual Conference on Computer Science Logic (CSL 2020) ## BibTeX citation@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 ## BibTeX citation@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}}, } |

JAR | Journal of Automated Reasoning August 1, 2019 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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) ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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) ## BibTeX citation@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. 2016 | October 17, 2016 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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}, url = {https://types22.inria.fr/files/2022/06/TYPES_2022_paper_49.pdf}, } |

TYPES '22 | 28th International Conference on Types for Proofs and Programs June 2022 ## BibTeX citation@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 ## BibTeX citation@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 '22 | 28th International Conference on Types for Proofs and Programs June 2022 ## BibTeX citation@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}, url = {https://types22.inria.fr/files/2022/06/TYPES_2022_paper_68.pdf}, } |

TYPES '22 | 28th International Conference on Types for Proofs and Programs June 2022 ## BibTeX citation@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}, } |

WITS '22 | Workshop on the Implementation of Type Systems (keynote) January 22, 2022 |

CT20→21 | |

MURI '20 | MURI Team Meeting 2020 March 2020 |

TYPES'18 | 24th International Conference on Types for Proofs and Programs (TYPES 2018) ## BibTeX citation@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}, } |

HoTT '19 | International Conference on Homotopy Type Theory, 2019 |

TYPES '19 | TYPES 2019 |

Aug. 2018 | Dagstuhl Seminar 18341: Formalization of Mathematics in Type Theory |

LFMTP '18 | International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP), 2018 ## BibTeX citation@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) ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@phdthesis{sterling:2021:thesis, author = {Sterling, Jonathan}, school = {Carnegie Mellon University}, year = {2021}, doi = {10.5281/zenodo.6990769}, note = {Version 1.1, revised May 2022}, number = {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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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 ## BibTeX citation@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}, } |