Vezzosi, Andrea; Mörtberg, Anders; Abel, Andreas Cubical Agda: a dependently typed programming language with univalence and higher inductive types. (English) Zbl 1512.68058 J. Funct. Program. 31, Paper No. e8, 47 p. (2021). MSC: 68N18 55U35 PDFBibTeX XMLCite \textit{A. Vezzosi} et al., J. Funct. Program. 31, Paper No. e8, 47 p. (2021; Zbl 1512.68058) Full Text: DOI
Brunerie, Guillaume The James construction and \(\pi _4(\mathbb{S}^{3})\) in homotopy type theory. (English) Zbl 1477.03035 J. Autom. Reasoning 63, No. 2, 255-284 (2019). MSC: 03B38 03B35 55U35 PDFBibTeX XMLCite \textit{G. Brunerie}, J. Autom. Reasoning 63, No. 2, 255--284 (2019; Zbl 1477.03035) Full Text: DOI arXiv
Romero, Ana; Rubio, Julio; Sergeraert, Francis An implementation of effective homotopy of fibrations. (English) Zbl 1436.55022 J. Symb. Comput. 94, 149-172 (2019). MSC: 55R05 68W30 PDFBibTeX XMLCite \textit{A. Romero} et al., J. Symb. Comput. 94, 149--172 (2019; Zbl 1436.55022) Full Text: DOI
Buchholtz, Ulrik; Hou Favonia, Kuen-Bang Cellular cohomology in homotopy type theory. (English) Zbl 1452.55016 Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9–12, 2018. New York, NY: Association for Computing Machinery (ACM). 521-529 (2018). MSC: 55U35 03B38 55N20 PDFBibTeX XMLCite \textit{U. Buchholtz} and \textit{K.-B. Hou Favonia}, in: Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9--12, 2018. New York, NY: Association for Computing Machinery (ACM). 521--529 (2018; Zbl 1452.55016) Full Text: DOI arXiv
van Doorn, Floris; von Raumer, Jakob; Buchholtz, Ulrik Homotopy type theory in Lean. (English) Zbl 1484.68319 Ayala-Rincón, Mauricio (ed.) et al., Interactive theorem proving. 8th international conference, ITP 2017, Brasília, Brazil, September 26–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10499, 479-495 (2017). MSC: 68V20 03B35 03B38 03G30 55U40 PDFBibTeX XMLCite \textit{F. van Doorn} et al., Lect. Notes Comput. Sci. 10499, 479--495 (2017; Zbl 1484.68319) Full Text: DOI arXiv
Capriotti, Paolo; Kraus, Nicolai; Vezzosi, Andrea Functions out of higher truncations. (English) Zbl 1373.03011 Kreutzer, Stephan (ed.), 24th EACSL annual conference and 29th workshop on computer science logic, CSL’15, Berlin, Germany, September 7–10, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-90-3). LIPIcs – Leibniz International Proceedings in Informatics 41, 359-373 (2015). MSC: 03B15 03G30 55U40 68T15 PDFBibTeX XMLCite \textit{P. Capriotti} et al., LIPIcs -- Leibniz Int. Proc. Inform. 41, 359--373 (2015; Zbl 1373.03011) Full Text: DOI arXiv
Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis Non-wellfounded trees in homotopy type theory. (English) Zbl 1433.03027 Altenkirch, Thorsten (ed.), 13th international conference on typed lambda calculi and applications, TLCA’15, Warsaw, Poland, July 1–3, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 38, 17-30 (2015). MSC: 03B38 03B35 55U35 PDFBibTeX XMLCite \textit{B. Ahrens} et al., LIPIcs -- Leibniz Int. Proc. Inform. 38, 17--30 (2015; Zbl 1433.03027) Full Text: DOI arXiv
Kraus, Nicolai; Sattler, Christian Higher homotopies in a hierarchy of univalent universes. (English) Zbl 1354.03100 ACM Trans. Comput. Log. 16, No. 2, Article No. 18, 12 p. (2015). MSC: 03G30 03B15 03B35 03B40 55U40 68T15 PDFBibTeX XMLCite \textit{N. Kraus} and \textit{C. Sattler}, ACM Trans. Comput. Log. 16, No. 2, Article No. 18, 12 p. (2015; Zbl 1354.03100) Full Text: DOI arXiv
Licata, Daniel R.; Finster, Eric Eilenberg-MacLane spaces in homotopy type theory. (English) Zbl 1395.68249 Proceedings of the joint meeting of the twenty-third EACSL annual conference on computer science logic, CSL, and the 2014 29th annual ACM/IEEE symposium on logic in computer science, LICS 2014, Vienna, Austria, July 14–18, 2014. Los Alamitos, CA: IEEE Computer Society (ISBN 978-1-4503-2886-9). Paper No. 66, 9 p. (2014). MSC: 68T15 03B15 55P20 PDFBibTeX XMLCite \textit{D. R. Licata} and \textit{E. Finster}, in: Proceedings of the joint meeting of the twenty-third EACSL annual conference on computer science logic, CSL, and the 2014 29th annual ACM/IEEE symposium on logic in computer science, LICS 2014, Vienna, Austria, July 14--18, 2014. Los Alamitos, CA: IEEE Computer Society. Paper No. 66, 9 p. (2014; Zbl 1395.68249) Full Text: DOI
Cockx, Jesper; Devriese, Dominique; Piessens, Frank Pattern matching without K. (English) Zbl 1345.68045 Proceedings of the 19th ACM SIGPLAN international conference on functional programming, ICFP ’14, Gothenburg, Sweden, September 1–3, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2873-9). 257-268 (2014). MSC: 68N18 03B15 03G30 55U40 PDFBibTeX XMLCite \textit{J. Cockx} et al., in: Proceedings of the 19th ACM SIGPLAN international conference on functional programming, ICFP '14, Gothenburg, Sweden, September 1--3, 2014. New York, NY: Association for Computing Machinery (ACM). 257--268 (2014; Zbl 1345.68045) Full Text: DOI Link
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten Generalizations of Hedberg’s theorem. (English) Zbl 1433.03032 Hasegawa, Masahito (ed.), Typed lambda calculi and applications. 11th international conference, TLCA 2013, Eindhoven, The Netherlands, June 26–28, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 7941, 173-188 (2013). MSC: 03B38 55U40 68V15 PDFBibTeX XMLCite \textit{N. Kraus} et al., Lect. Notes Comput. Sci. 7941, 173--188 (2013; Zbl 1433.03032) Full Text: DOI