Kraus, Nicolai; Nordvall Forsberg, Fredrik; Xu, Chuangjie Type-theoretic approaches to ordinals. (English) Zbl 07679991 Theor. Comput. Sci. 957, Article ID 113843, 34 p. (2023). MSC: 03-XX PDFBibTeX XMLCite \textit{N. Kraus} et al., Theor. Comput. Sci. 957, Article ID 113843, 34 p. (2023; Zbl 07679991) Full Text: DOI arXiv
Boulier, Simon; Tabareau, Nicolas Model structure on the universe of all types in interval type theory. (English) Zbl 07460115 Math. Struct. Comput. Sci. 31, No. 4, 392-423 (2021). MSC: 03B38 55U35 18N45 PDFBibTeX XMLCite \textit{S. Boulier} and \textit{N. Tabareau}, Math. Struct. Comput. Sci. 31, No. 4, 392--423 (2021; Zbl 07460115) Full Text: DOI
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
Booij, Auke B. Extensional constructive real analysis via locators. (English) Zbl 07408496 Math. Struct. Comput. Sci. 31, No. 1, 64-88 (2021). MSC: 03B38 03F60 PDFBibTeX XMLCite \textit{A. B. Booij}, Math. Struct. Comput. Sci. 31, No. 1, 64--88 (2021; Zbl 07408496) Full Text: DOI arXiv
Veltri, Niccolò; van der Weide, Niels Constructing higher inductive types as groupoid quotients. (English) Zbl 1498.03037 Log. Methods Comput. Sci. 17, No. 2, Paper No. 8, 42 p. (2021). MSC: 03B38 18N10 55U35 PDFBibTeX XMLCite \textit{N. Veltri} and \textit{N. van der Weide}, Log. Methods Comput. Sci. 17, No. 2, Paper No. 8, 42 p. (2021; Zbl 1498.03037) Full Text: arXiv Link
Piceghello, Stefano Coherence for monoidal groupoids in HoTT. (English) Zbl 07756113 Bezem, Marc (ed.) et al., 25th international conference on types for proofs and programs. TYPES 2019, June 11–14, 2019, Oslo, Norway. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 175, Article 8, 20 p. (2020). MSC: 03B70 68N30 PDFBibTeX XMLCite \textit{S. Piceghello}, LIPIcs -- Leibniz Int. Proc. Inform. 175, Article 8, 20 p. (2020; Zbl 07756113) Full Text: DOI
van der Weide, Niels Constructing higher inductive types as groupoid quotients. (English) Zbl 1498.03036 Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 929-943 (2020). MSC: 03B38 18N10 55U35 PDFBibTeX XMLCite \textit{N. van der Weide}, in: Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8--11, 2020. New York, NY: Association for Computing Machinery (ACM). 929--943 (2020; Zbl 1498.03036) Full Text: DOI
van den Berg, Benno Univalent polymorphism. (English) Zbl 1440.18048 Ann. Pure Appl. Logic 171, No. 6, Article ID 102793, 29 p. (2020). Reviewer: Hirokazu Nishimura (Tsukuba) MSC: 18N45 03B38 03F50 03G30 18C50 55U35 68Q55 PDFBibTeX XMLCite \textit{B. van den Berg}, Ann. Pure Appl. Logic 171, No. 6, Article ID 102793, 29 p. (2020; Zbl 1440.18048) Full Text: DOI arXiv
Mainzer, Klaus From mathesis universalis to provability, computability, and constructivity. (English) Zbl 1469.03113 Centrone, Stefania (ed.) et al., Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. Cham: Springer. Synth. Libr. 412, 203-234 (2019). MSC: 03D10 03D35 03F35 03F60 03B30 03F25 68V15 03B38 55U40 PDFBibTeX XMLCite \textit{K. Mainzer}, Synth. Libr. 412, 203--234 (2019; Zbl 1469.03113) Full Text: DOI
Awodey, Steve Mathesis universalis and homotopy type theory. (English) Zbl 1469.03035 Centrone, Stefania (ed.) et al., Mathesis universalis, computability and proof. Based on the Humboldt-Kolleg “Proof theory as mathesis universalis”, held at the German-Italian Centre for European Excellence, Villa Vigoni, Loveno di Menaggio, Como, Italy, July 24–28, 2017. Cham: Springer. Synth. Libr. 412, 13-36 (2019). MSC: 03B38 55U40 PDFBibTeX XMLCite \textit{S. Awodey}, Synth. Libr. 412, 13--36 (2019; Zbl 1469.03035) Full Text: DOI
Ahrens, Benedikt; Matthes, Ralph; Mörtberg, Anders From signatures to monads in UniMath. (English) Zbl 1468.03007 J. Autom. Reasoning 63, No. 2, 285-318 (2019). MSC: 03B35 03B38 18C10 18C15 55U35 68V20 PDFBibTeX XMLCite \textit{B. Ahrens} et al., J. Autom. Reasoning 63, No. 2, 285--318 (2019; Zbl 1468.03007) Full Text: DOI arXiv
Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea Guarded cubical type theory. (English) Zbl 1477.03034 J. Autom. Reasoning 63, No. 2, 211-253 (2019). MSC: 03B38 55U35 18F20 PDFBibTeX XMLCite \textit{L. Birkedal} et al., J. Autom. Reasoning 63, No. 2, 211--253 (2019; Zbl 1477.03034) Full Text: DOI arXiv Link
Grayson, Daniel R. An introduction to univalent foundations for mathematicians. (English) Zbl 1461.03012 Bull. Am. Math. Soc., New Ser. 55, No. 4, 427-450 (2018). MSC: 03B38 03B35 03G30 18A15 55U35 PDFBibTeX XMLCite \textit{D. R. Grayson}, Bull. Am. Math. Soc., New Ser. 55, No. 4, 427--450 (2018; Zbl 1461.03012) Full Text: DOI arXiv
Ahrens, Benedikt; Lumsdaine, Peter Lefanu; Voevodsky, Vladimir Categorical structures for type theory in univalent foundations. (English) Zbl 1496.03053 Log. Methods Comput. Sci. 14, No. 3, Paper No. 18, 18 p. (2018). MSC: 03B38 03F50 18C50 03B70 55U40 68V15 PDFBibTeX XMLCite \textit{B. Ahrens} et al., Log. Methods Comput. Sci. 14, No. 3, Paper No. 18, 18 p. (2018; Zbl 1496.03053) Full Text: DOI arXiv
Angiuli, Carlo; Harper, Robert Meaning explanations at higher dimension. (English) Zbl 1436.03102 Indag. Math., New Ser. 29, No. 1, 135-149 (2018). MSC: 03B38 55U35 PDFBibTeX XMLCite \textit{C. Angiuli} and \textit{R. Harper}, Indag. Math., New Ser. 29, No. 1, 135--149 (2018; Zbl 1436.03102) Full Text: DOI
Mainzer, Klaus The digital and the real world. Computational foundations of mathematics, science, technology, and philosophy. With booklet ‘Supplements and corrections’. (English) Zbl 1411.68007 Hackensack, NJ: World Scientific (ISBN 978-981-3225-48-0/hbk; 978-981-3225-50-3/ebook). x, 460 p., 16 p./booklet (2018). Reviewer: Manfred Kerber (Birmingham) MSC: 68-02 03-02 00A05 03B70 68Qxx PDFBibTeX XMLCite \textit{K. Mainzer}, The digital and the real world. Computational foundations of mathematics, science, technology, and philosophy. With booklet `Supplements and corrections'. Hackensack, NJ: World Scientific (2018; Zbl 1411.68007) Full Text: DOI
Ahrens, Benedikt; Lumsdaine, Peter LeFanu; Voevodsky, Vladimir Categorical structures for type theory in univalent foundations. (English) Zbl 1528.03100 Goranko, Valentin (ed.) et al., 26th EACSL annual conference on computer science logic, CSL 2017, Stockholm, Sweden, August 20–24, 2017. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 82, Article 8, 16 p. (2017). MSC: 03B38 03F50 03B70 18C50 55U40 68V15 PDFBibTeX XMLCite \textit{B. Ahrens} et al., LIPIcs -- Leibniz Int. Proc. Inform. 82, Article 8, 16 p. (2017; Zbl 1528.03100) Full Text: DOI
Cockx, Jesper; Devriese, Dominique; Piessens, Frank Eliminating dependent pattern matching without K. (English) Zbl 1419.68037 J. Funct. Program. 26, Paper No. e16, 40 p. (2016). MSC: 68N18 03B15 03G30 55U40 PDFBibTeX XMLCite \textit{J. Cockx} et al., J. Funct. Program. 26, Paper No. e16, 40 p. (2016; Zbl 1419.68037) Full Text: DOI
Timany, Amin; Jacobs, Bart Category theory in Coq 8.5. (English) Zbl 1387.68208 Kesner, Delia (ed.) et al., 1st international conference on formal structures for computation and deduction, FSCD 2016, Porto, Portugal, June 22–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-010-1). LIPIcs – Leibniz International Proceedings in Informatics 52, Article 30, 18 p. (2016). MSC: 68T15 03B15 03G30 18A99 55U40 PDFBibTeX XMLCite \textit{A. Timany} and \textit{B. Jacobs}, LIPIcs -- Leibniz Int. Proc. Inform. 52, Article 30, 18 p. (2016; Zbl 1387.68208) Full Text: DOI arXiv
Birkedal, Lars; Bizjak, Aleš; Clouston, Ranald; Grathwohl, Hans Bugge; Spitters, Bas; Vezzosi, Andrea Guarded cubical type theory: path equality for guarded recursion. (English) Zbl 1370.68052 Regnier, Laurent (ed.) et al., 25th EACSL annual conference and 30th workshop on computer science logic, CSL’16, Marseille, France, August 29 – September 1, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-022-4). LIPIcs – Leibniz International Proceedings in Informatics 62, Article 23, 17 p. (2016). MSC: 68N30 03B15 03B70 03G30 55U40 68Q55 68T15 PDFBibTeX XMLCite \textit{L. Birkedal} et al., LIPIcs -- Leibniz Int. Proc. Inform. 62, Article 23, 17~p. (2016; Zbl 1370.68052) Full Text: DOI arXiv
Sojakova, Kristina The equivalence of the torus and the product of two circles in homotopy type theory. (English) Zbl 1367.03018 ACM Trans. Comput. Log. 17, No. 4, Article No. 29, 19 p. (2016). MSC: 03B15 03G30 55U40 PDFBibTeX XMLCite \textit{K. Sojakova}, ACM Trans. Comput. Log. 17, No. 4, Article No. 29, 19 p. (2016; Zbl 1367.03018) Full Text: DOI arXiv
Shulman, Michael Idempotents in intensional type theory. (English) Zbl 1445.03011 Log. Methods Comput. Sci. 12, No. 3, Paper No. 9, 24 p. (2016). MSC: 03B38 03G30 18N60 55U40 PDFBibTeX XMLCite \textit{M. Shulman}, Log. Methods Comput. Sci. 12, No. 3, Paper No. 9, 24 p. (2016; Zbl 1445.03011) Full Text: DOI arXiv Backlinks: MO
Hirschowitz, André; Hirschowitz, Tom; Tabareau, Nicolas Wild \(\omega\)-categories for the homotopy hypothesis in type theory. (English) Zbl 1433.03031 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, 226-240 (2015). MSC: 03B38 03G30 18N10 18M60 PDFBibTeX XMLCite \textit{A. Hirschowitz} et al., LIPIcs -- Leibniz Int. Proc. Inform. 38, 226--240 (2015; Zbl 1433.03031) Full Text: DOI
Sojakova, Kristina Higher inductive types as homotopy-initial algebras. (English) Zbl 1345.03017 Proceedings of the 42nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’15, Mumbai, India, January 12–18, 2015. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3300-9). 31-42 (2015). MSC: 03B15 03G30 55U40 PDFBibTeX XMLCite \textit{K. Sojakova}, in: Proceedings of the 42nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL '15, Mumbai, India, January 12--18, 2015. New York, NY: Association for Computing Machinery (ACM). 31--42 (2015; Zbl 1345.03017) Full Text: DOI arXiv
Avigad, Jeremy; Kapulkin, Krzysztof; Lumsdaine, Peter LeFanu Homotopy limits in type theory. (English) Zbl 1362.18004 Math. Struct. Comput. Sci. 25, No. 5, 1040-1070 (2015). MSC: 18A15 03B15 55U40 68T15 PDFBibTeX XMLCite \textit{J. Avigad} et al., Math. Struct. Comput. Sci. 25, No. 5, 1040--1070 (2015; Zbl 1362.18004) 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
Pelayo, Álvaro; Warren, Michael A. Homotopy type theory and Voevodsky’s univalent foundations. (English) Zbl 1432.03019 Bull. Am. Math. Soc., New Ser. 51, No. 4, 597-648 (2014). MSC: 03B38 18N45 03G30 55U40 55U35 68N18 PDFBibTeX XMLCite \textit{Á. Pelayo} and \textit{M. A. Warren}, Bull. Am. Math. Soc., New Ser. 51, No. 4, 597--648 (2014; Zbl 1432.03019) Full Text: DOI arXiv
Gross, Jason; Chlipala, Adam; Spivak, David I. Experience implementing a performant category-theory library in Coq. (English) Zbl 1416.68163 Klein, Gerwin (ed.) et al., Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14–17, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8558, 275-291 (2014). MSC: 68T15 18-04 PDFBibTeX XMLCite \textit{J. Gross} et al., Lect. Notes Comput. Sci. 8558, 275--291 (2014; Zbl 1416.68163) Full Text: DOI arXiv
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
Awodey, Steve; Gambino, Nicola; Sojakova, Kristina Inductive types in homotopy type theory. (English) Zbl 1364.03014 Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25–28, 2012. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-4769-5). 95-104 (2012). MSC: 03B15 03G30 18C10 55U40 68T15 PDFBibTeX XMLCite \textit{S. Awodey} et al., in: Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25--28, 2012. Los Alamitos, CA: IEEE Computer Society. 95--104 (2012; Zbl 1364.03014) Full Text: DOI arXiv
Licata, Daniel R.; Harper, Robert 2-dimensional directed type theory. (English) Zbl 1343.03051 Mislove, Michael (ed.) et al., Proceedings of the 27th conference on the mathematical foundations of programming semantics (MFPS XXVII), Pittsburgh, PA, USA, May 25–28, 2011. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 276, 263-289 (2011). MSC: 03G30 03B15 18D05 55U40 68N30 PDFBibTeX XMLCite \textit{D. R. Licata} and \textit{R. Harper}, Electron. Notes Theor. Comput. Sci. 276, 263--289 (2011; Zbl 1343.03051) Full Text: DOI
Voevodsky, Vladimir Univalent semantics of constructive type theories. (English) Zbl 1250.03121 Jouannaud, Jean-Pierre (ed.) et al., Certified programs and proofs. First international conference, CPP 2011, Kenting, Taiwan, December 7–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-25378-2/pbk). Lecture Notes in Computer Science 7086, 70 (2011). MSC: 03F50 03B15 55U40 68T15 PDFBibTeX XMLCite \textit{V. Voevodsky}, Lect. Notes Comput. Sci. 7086, 70 (2011; Zbl 1250.03121) Full Text: DOI
Voevodsky, Vladimir Univalent foundations of mathematics. (English) Zbl 1371.03097 Beklemishev, Lev D. (ed.) et al., Logic, language, information and computation. 18th international workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18–20, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-20919-2/pbk). Lecture Notes in Computer Science 6642. Lecture Notes in Artificial Intelligence, 4 (2011). MSC: 03F50 03B15 55U35 55U40 68T15 PDFBibTeX XMLCite \textit{V. Voevodsky}, Lect. Notes Comput. Sci. 6642, 4 (2011; Zbl 1371.03097) Full Text: DOI