On programming in homotopy type theory:

*Programming in Homotopy Type Theory*, Talk at IFIP Wroking Group 2.8 meeting, November, 2012 (pdf, pdf)

Introduction to basics of synthetic homotopy theory in terms of homotopy type theory:

- Guillaume Brunerie, Dan Licata, Peter LeFanu Lumsdaine:
*Homotopy theory in type theory*, 2013 (pdf slides, pdf, blog entry 1, blog entry 2)

Formalization of (the proof of) the Blakers-Massey theorem in homotopy type theory:

- Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine,
*A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory*, LICS ‘16 (2016) 565–574 [arXiv.1605.03227, doi:10.1145/2933575.2934545]

On adjoint logic:

- Daniel Licata, Mike Shulman, and Mitchell Riley,
*A Fibrational Framework for Substructural and Modal Logics (extended version)*, in Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (doi: 10.4230/LIPIcs.FSCD.2017.25, pdf)

On synthetic (∞,1)-category theory in cubical type theory with bicubical sets:

- Matthew Weaver, Daniel Licata,
*A Constructive Model of Directed Univalence in Bicubical Sets*, in:*Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’20*, Association for Computing Machinery (2020) 915–928 [doi:10.1145/3373718.3394794]

On homotopy dependent linear type theory of dependent stable homotopy types with categorical semantics in parametrized spectra:

- Mitchell Riley, Eric Finster, Daniel Licata,
*Synthetic Spectra via a Monadic and Comonadic Modality*(arXiv:2102.04099)

category: people

Last revised on October 14, 2023 at 06:27:25. See the history of this page for a list of all contributions to it.