| Eilenberg-MacLane spaces in homotopy type theory DR Licata, E Finster Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference …, 2014 | 84 | 2014 |
| A generalized Blakers–Massey theorem M Anel, G Biedermann, E Finster, A Joyal Journal of Topology 13 (4), 1521-1553, 2020 | 70 | 2020 |
| A type-theoretical definition of weak ω-categories E Finster, S Mimram 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-12, 2017 | 50 | 2017 |
| Goodwillie's calculus of functors and higher topos theory M Anel, G Biedermann, E Finster, A Joyal Journal of topology 11 (4), 1100-1132, 2018 | 23 | 2018 |
| A type theory for strictly unital∞-categories E Finster, D Reutter, J Vicary, A Rice Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer …, 2022 | 19 | 2022 |
| Left-exact localizations of∞-topoi I: Higher sheaves M Anel, G Biedermann, E Finster, A Joyal Advances in Mathematics 400, 108268, 2022 | 17 | 2022 |
| A mechanization of the Blakers-Massey connectivity theorem in homotopy type theory KB Hou, E Finster, DR Licata, PLF Lumsdaine Proceedings of the 31st annual ACM/IEEE symposium on logic in computer …, 2016 | 17 | 2016 |
| Synthetic spectra via a monadic and comonadic modality M Riley, E Finster, DR Licata arXiv preprint arXiv:2102.04099, 2021 | 14 | 2021 |
| Globular weak -categories as models of a type theory T Benjamin, E Finster, S Mimram arXiv preprint arXiv:2106.04475, 2021 | 9 | 2021 |
| Computads for weak ω-categories as an inductive type CJ Dean, E Finster, I Markakis, D Reutter, J Vicary Advances in Mathematics 450, 109739, 2024 | 8 | 2024 |
| A cartesian bicategory of polynomial functors in homotopy type theory E Finster, S Mimram, M Lucas, T Seiller arXiv preprint arXiv:2112.14050, 2021 | 8 | 2021 |
| Eilenberg–MacLane spaces in homotopy type theory. LICS, 2014 D Licata, E Finster | 7 | |
| Types are internal∞-groupoids A Allioux, E Finster, M Sozeau Draft paper. Available online at https://ericfinster. github. io/files/type …, 2021 | 5 | 2021 |
| The CaTT proof assistant, 2018 T Benjamin, E Finster, S Mimram | 5 | |
| A type theory for strictly associative infinity categories E Finster, A Rice, J Vicary arXiv preprint arXiv:2109.01513, 2021 | 4 | 2021 |
| Types are internal∞-groupoids E Finster, A Allioux, M Sozeau 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1-13, 2021 | 3 | 2021 |
| Left-exact localizations of∞-topoi II: Grothendieck topologies M Anel, G Biedermann, E Finster, A Joyal Journal of Pure and Applied Algebra 228 (3), 107472, 2024 | 2 | 2024 |
| New methods for left exact localisations of topoi M Anel, G Biedermann, E Finster, A Joyal preparation; slides at http://mathieu. anel. free. fr/mat/doc/Anel …, 2019 | 2 | 2019 |
| Homotopy Type Theory: Univalent Foundations of Mathematics P Aczel, B Ahrens, T Altenkirch, S Awodey, B Barras, A Bauer, Y Bertot, ... Aucun, 2013 | 2 | 2013 |
| Type theory and the opetopes E Finster talk presented at the Polish Seminar on Category Theory and its Applications, 2012 | 2 | 2012 |
