research-article

The lean mathematical library

Corporate:

The mathlib CommunityAuthors Info & Claims

CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

Pages 367 - 381

https://doi.org/10.1145/3372885.3373824

Published: 22 January 2020 Publication History

Abstract

This paper describes mathlib, a community-driven effort to build a unified library of mathematics formalized in the Lean proof assistant. Among proof assistant libraries, it is distinguished by its dependently typed foundations, focus on classical mathematics, extensive hierarchy of structures, use of large- and small-scale automation, and distributed organization. We explain the architecture and design decisions of the library and the social organization that has led to its development.

References

[1]

1994. The QED Manifesto. In Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings . 238–251. http://link.springer.com/chapter/ 10.1007/3-540-58156-1_17

[2]

Reynald Affeldt, Cyril Cohen, and Damien Rouhling. 2018. Formalization Techniques for Asymptotic Reasoning in Classical Analysis. J. Formalized Reasoning 11, 1 (2018), 43–76.

[3]

Jesús Aransay and Jose Divasón. 2014. Formalization and Execution of Linear Algebra: From Theorems to Algorithms. In Logic-Based Program Synthesis and Transformation, Gopal Gupta and Ricardo Peña (Eds.). Springer International Publishing, Cham, 1–18.

[4]

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. 2009. Hints in Unification. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings . 84–98.

Digital Library

[5]

Jeremy Avigad, Leonardo de Moura, and Soonho Kong. 2014. Theorem Proving in Lean . Carnegie Mellon University.

[6]

Seulkee Baek. 2019. Reflected Decision Procedures in Lean. Master’s thesis. Carnegie Mellon University. http://www.andrew.cmu.edu/ user/avigad/Students/baek_ms_thesis.pdf

[7]

Clemens Ballarin. 2003. Locales and Locale Expressions in Isabelle/Isar. In Types for Proofs and Programs, International Workshop, TYPES 2003, Torino, Italy, April 30 - May 4, 2003, Revised Selected Papers . 34–50.

[8]

Grzegorz Bancerek, Czeslaw Bylinski, Adam Grabowski, Artur Kornilowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak. 2018. The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar. J. Autom. Reasoning 61, 1-4 (2018), 9–32.

Digital Library

[9]

Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. 2015. Mizar: State-of-the-art and Beyond. In Intelligent Computer Mathematics, Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (Eds.). Springer International Publishing, Cham, 261–279.

Digital Library

[10]

Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions . Springer.

[11]

Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. 2013. Extending Sledgehammer with SMT Solvers. J. Autom. Reasoning 51, 1 (2013), 109–128.

[12]

Jasmin Christian Blanchette, Max W. Haslbeck, Daniel Matichuk, and Tobias Nipkow. 2015. Mining the Archive of Formal Proofs. In Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13-17, 2015, Proceedings . 3–17.

Digital Library

[13]

Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. 2016. Hammering towards QED. J. Formalized Reasoning 9, 1 (2016), 101–148.

[14]

Sylvie Boldo, Catherine Lelay, and Guillaume Melquiond. 2015. Coquelicot: A User-Friendly Library of Real Analysis for Coq. Mathematics in Computer Science 9, 1 (2015), 41–62.

[15]

Kevin Buzzard, Johan Commelin, and Patrick Massot. 2020. Formalising Perfectoid Spaces. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, January 20-21, 2020 .

Digital Library

[16]

Mario Carneiro. 2019. Formalizing Computability Theory via Partial Recursive Functions. In 10th International Conference on Interactive Theorem Proving (ITP 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), John Harrison, John O’Leary, and Andrew Tolmach (Eds.), Vol. 141. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 12:1–12:17.

[17]

Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. 1986. Implementing mathematics with the Nuprl proof development system . Prentice Hall. http://dl.acm.org/citation.cfm?id=10510

[18]

Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. 2019. Formalizing the Solution to the Cap Set Problem. In 10th International Conference on Interactive Theorem Proving (ITP 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), John Harrison, John O’Leary, and Andrew Tolmach (Eds.), Vol. 141. Schloss Dagstuhl– Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 15:1–15:19.

[19]

Leonardo de Moura and Nikolaj Bjørner. 2007. Efficient E-Matching for SMT Solvers. In Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings . 183–198.

Digital Library

[20]

Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (system description). https://leanprover.github.io/papers/system.pdf

[21]

Jose Divasón and Jesús Aransay. 2013. Rank-Nullity Theorem in Linear Algebra. Archive of Formal Proofs (Jan. 2013). http://isa-afp.org/entries/ Rank_Nullity_Theorem.html, Formal proof development.

[22]

Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. 2017. A metaprogramming framework for formal verification. PACMPL 1, ICFP (2017), 34:1–34:29.

Digital Library

[23]

Jordan S. Ellenberg and Dion Gijswijt. 2017. On large subsets of F n q with no three-term arithmetic progression. Ann. of Math. (2) 185, 1 (2017), 339–343.

[24]

François Garillot, Georges Gonthier, Assia Mahboubi, and Laurence Rideau. 2009. Packaging Mathematical Structures. In Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings . 327–342.

Digital Library

[25]

Michèle Giry. 1982. A categorical approach to probability theory. In Categorical aspects of topology and analysis (Ottawa, Ont., 1980). Lecture Notes in Math., Vol. 915. Springer, Berlin-New York, 68–85.

[26]

Georges Gonthier. 2011. Point-Free, Set-Free Concrete Linear Algebra. In Interactive Theorem Proving, Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 103–118.

[27]

Georges Gonthier and Assia Mahboubi. 2010. An introduction to small scale reflection in Coq. J. Formalized Reasoning 3, 2 (2010), 95–152.

[28]

Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. 2010. Mizar in a Nutshell. Journal of Formalized Reasoning 3, 2 (2010), 153– 245.

[29]

Adam Grabowski, Artur Kornilowicz, and Christoph Schwarzweller. 2016. On algebraic hierarchies in mathematical repository of Mizar. In Proceedings of the 2016 Federated Conference on Computer Science and Information Systems, FedCSIS 2016, Gdańsk, Poland, September 11-14, 2016. 363–371.

[30]

Benjamin Grégoire and Assia Mahboubi. 2005. Proving Equalities in a Commutative Ring Done Right in Coq. In Theorem Proving in Higher Order Logics, Joe Hurd and Tom Melham (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 98–113.

Digital Library

[31]

Florian Haftmann and Makarius Wenzel. 2006. Constructive type classes in Isabelle. In International Workshop on Types for Proofs and Programs . Springer, 160–174.

[32]

Thomas C. Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason M. Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu, and Roland Zumkeller. 2017. A Formal Proof of the Kepler Conjecture. Forum of Mathematics, Pi 5 (2017), e2.

[33]

Jesse Michael Han and Floris van Doorn. 2019. A Formalization of Forcing and the Unprovability of the Continuum Hypothesis. In 10th International Conference on Interactive Theorem Proving (ITP 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), John Harrison, John O’Leary, and Andrew Tolmach (Eds.), Vol. 141. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 19:1– 19:19.

[34]

Jesse Michael Han and Floris van Doorn. 2020. A Formal Proof of the Independence of the Continuum Hypothesis. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, January 20-21, 2020 .

Digital Library

[35]

John Harrison. 2009. HOL Light: An Overview. In Theorem Proving in Higher Order Logics, Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 60–66.

Digital Library

[36]

John Harrison. 2013. The HOL Light Theory of Euclidean Space. J. Autom. Reasoning 50, 2 (2013), 173–190.

Digital Library

[37]

Hao Huang. 2019. Induced subgraphs of hypercubes and a proof of the Sensitivity Conjecture. arXiv preprint arXiv:1907.00847 (2019).

[38]

Fabian Immler and Bohua Zhan. 2019. Smooth manifolds and types to sets for linear algebra in Isabelle/HOL. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019 . 65–77.

Digital Library

[39]

C. Kaliszyk and K. Pąk. 2017. Progress in the independent certification of mizar mathematical library in isabelle. In 2017 Federated Conference on Computer Science and Information Systems (FedCSIS) . 227–236.

[40]

Cezary Kaliszyk, Karol Pąk, and Josef Urban. 2016. Towards a Mizar Environment for Isabelle: Foundations and Language. In Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016) . ACM, New York, NY, USA, 58–65.

Digital Library

[41]

Florian Kammüller, Markus Wenzel, and Lawrence C. Paulson. 1999. Locales - A Sectioning Concept for Isabelle. In Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs’99, Nice, France, September, 1999, Proceedings . 149–166.

[42]

M. Kaufmann, P. Manolios, and J.S. Moore. 2000. Computer-Aided Reasoning: ACL2 Case Studies . Advances in Formal Methods, Vol. 4. Springer US.

[43]

Holden Lee. 2014. Vector Spaces. Archive of Formal Proofs (2014). http: //isa-afp.org/entries/VectorSpace.html, Formal proof development.

[44]

Robert Y. Lewis. 2019. A formal proof of Hensel’s lemma over the p-adic integers. In Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019 . 15–26.

Digital Library

[45]

Paul-Nicolas Madelaine. 2019. Arithmetic and casting in Lean. Technical Report. Vrije Universiteit Amsterdam. https://lean-forward.github. io/internships/arithmetic_and_casting_in_lean.pdf

[46]

Assia Mahboubi and Enrico Tassi. 2017. Mathematical Components. https://math-comp.github.io/mcb/

[47]

Norman Megill and David A. Wheeler. 2019. Metamath: A Computer Language for Mathematical Proofs . Lulu Press.

[48]

Walther Neuper. 2019. Technologies for "Complete, Transparent & Interactive Models of Math" in Education. Electronic Proceedings in Theoretical Computer Science 290 (03 2019), 76–95.

[49]

Tobias Nipkow, Lawrence C Paulson, and Markus Wenzel. 2002. Isabelle/HOL: a proof assistant for higher-order logic . Vol. 2283. Springer Science & Business Media.

[50]

Sam Owre, John M. Rushby, and Natarajan Shankar. 1992. PVS: A Prototype Verification System. In Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings . 748–752.

[51]

Karol Pak. 2016. Topological Foundations for a Formal Theory of Manifolds. In Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016 . 14–16. http://ceur-ws.org/Vol-1785/F4.pdf

[52]

Frank Pfenning and Christine Paulin-Mohring. 1989. Inductively Defined Types in the Calculus of Constructions. In Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29 - April 1, 1989, Proceedings . 209–228.

[53]

William Pugh. 1991. The Omega Test: A Fast and Practical Integer Programming Algorithm for Dependence Analysis. In Proceedings of the 1991 ACM/IEEE Conference on Supercomputing (Supercomputing ’91) . ACM, New York, NY, USA, 4–13.

Digital Library

[54]

Daniel Selsam and Leonardo Moura. 2016. Congruence Closure in Intensional Type Theory. In Proceedings of the 8th International Joint Conference on Automated Reasoning - Volume 9706 . Springer-Verlag, Berlin, Heidelberg, 99–115.

Digital Library

[55]

Konrad Slind and Michael Norrish. 2008. A Brief Overview of HOL4. In Theorem Proving in Higher Order Logics, Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 28–32.

Digital Library

[56]

Bas Spitters and Eelis van der Weegen. 2011. Type classes for mathematics in type theory. Mathematical Structures in Computer Science 21, 4 (2011), 795–825.

[57]

Sebastian Ullrich and Leonardo de Moura. 2019. Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming. arXiv: cs.PL/1908.05647

[58]

Josef Urban and Geoff Sutcliffe. 2008. ATP-based Cross-Verification of Mizar Proofs: Method, Systems, and First Experiments. Mathematics in Computer Science 2, 2 (2008), 231–251.

[59]

Philip Wadler and Stephen Blott. 1989. How to Make ad-hoc Polymorphism Less ad-hoc. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989 . 60–76.

Digital Library

[60]

Markus Wenzel. 1997. Type Classes and Overloading in Higher-Order Logic. In Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs’97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings . 307–322.

[61]

H. P. Williams. 1986. Fourier’s Method of Linear Programming and Its Dual. The American Mathematical Monthly 93, 9 (1986), 681–695. http://www.jstor.org/stable/2322281

[62]

Minchao Wu and Rajeev Goré. 2019. Verified Decision Procedures for Modal Logics. In 10th International Conference on Interactive Theorem Proving (ITP 2019) (Leibniz International Proceedings in Informatics (LIPIcs)), John Harrison, John O’Leary, and Andrew Tolmach (Eds.), Vol. 141. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 31:1–31:19.

Cited By

Bernstein D(2024)Understanding binary-Goppa decodingIACR Communications in Cryptology10.62056/angy4fe-3Online publication date: 9-Apr-2024
https://doi.org/10.62056/angy4fe-3
de Lima TBorges Avelar AGaldino AAyala-Rincón M(2024)Formalizing Factorization on Euclidean Domains and Abstract Euclidean AlgorithmsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.402.5402(18-33)Online publication date: 23-Apr-2024
https://doi.org/10.4204/EPTCS.402.5
Appenzeller R(2024)(In)dependence of the axioms of Λ-treesAnalysis and Geometry in Metric Spaces10.1515/agms-2023-010612:1Online publication date: 1-Apr-2024
https://doi.org/10.1515/agms-2023-0106
Show More Cited By

Index Terms

The lean mathematical library
1. Mathematics of computing
  1. Mathematical software
2. Security and privacy
  1. Formal methods and theory of security
    1. Logic and verification

Recommendations

Survey on agile and lean usage in finnish software industry
ESEM '12: Proceedings of the ACM-IEEE international symposium on Empirical software engineering and measurement

Earlier empirical studies have demonstrated the interest that agile methods have generated in the software industry. Currently, lean approaches are increasingly adopted for complementing agile methods in software processes. With the goal of providing up-...
Lean Software Development: A Tutorial

“Lean Software Development” has become a popular term over the last few years. This tutorial describes where it comes from, what it means, how it relates to well-known agile development practices, and how it will evolve in the future.
Facilitating Agile Software Development with Lean Architecture in the DCI Paradigm
ITNG '12: Proceedings of the 2012 Ninth International Conference on Information Technology - New Generations

Both agile software development and lean architecture have been studied in the software engineering field. Combining these two approaches has also been investigated. However, the existing research and practices only present the principles but fail to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs

January 2020

381 pages

ISBN:9781450370974

DOI:10.1145/3372885

Program Chairs:
Jasmin Blanchette
Universiteit Amsterdam, Netherlands
,
Cătălin Hriţcu
Inria, France

Copyright © 2020 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

In-Cooperation

SIGLOG: ACM Special Interest Group on Logic and Computation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 January 2020

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

POPL '20

Sponsor:

SIGPLAN

POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 20 - 21, 2020

LA, New Orleans, USA

Acceptance Rates

Overall Acceptance Rate 18 of 26 submissions, 69%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

66
Total Citations
View Citations
368
Total Downloads

Downloads (Last 12 months)61
Downloads (Last 6 weeks)10

Reflects downloads up to 17 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Bernstein D(2024)Understanding binary-Goppa decodingIACR Communications in Cryptology10.62056/angy4fe-3Online publication date: 9-Apr-2024
https://doi.org/10.62056/angy4fe-3
de Lima TBorges Avelar AGaldino AAyala-Rincón M(2024)Formalizing Factorization on Euclidean Domains and Abstract Euclidean AlgorithmsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.402.5402(18-33)Online publication date: 23-Apr-2024
https://doi.org/10.4204/EPTCS.402.5
Appenzeller R(2024)(In)dependence of the axioms of Λ-treesAnalysis and Geometry in Metric Spaces10.1515/agms-2023-010612:1Online publication date: 1-Apr-2024
https://doi.org/10.1515/agms-2023-0106
Laufer EOzdemir ABoneh DLuo BLiao XXu JKirda ELie D(2024)zkPi: Proving Lean Theorems in Zero-KnowledgeProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security10.1145/3658644.3670322(4301-4315)Online publication date: 2-Dec-2024
https://dl.acm.org/doi/10.1145/3658644.3670322
Lincroft GCho MHough KBazzaz MBell JSpinellis DConstantinou EBacchelli A(2024)Thirty-Three Years of Mathematicians and Software Engineers: A Case Study of Domain Expertise and Participation in Proof Assistant EcosystemsProceedings of the 21st International Conference on Mining Software Repositories10.1145/3643991.3644908(1-13)Online publication date: 15-Apr-2024
https://dl.acm.org/doi/10.1145/3643991.3644908
Ahrens BMatthes Rvan der Weide NWullaert KTimany ATraytel DPientka BBlazy S(2024)Displayed Monoidal Categories for the Semantics of Linear LogicProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636956(260-273)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636956
van der Weide NRasekh NAhrens BNorth PTimany ATraytel DPientka BBlazy S(2024)Univalent Double CategoriesProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636955(246-259)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636955
Gadgil STadipatri ATimany ATraytel DPientka BBlazy S(2024)Formalizing Giles Gardam’s Disproof of Kaplansky’s Unit ConjectureProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636947(177-189)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636947
Edmonds CPaulson LTimany ATraytel DPientka BBlazy S(2024)Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local LemmaProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636946(132-146)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636946
Kudasov NRiehl EWeinberger JTimany ATraytel DPientka BBlazy S(2024)Formalizing the ∞-Categorical Yoneda LemmaProceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs10.1145/3636501.3636945(274-290)Online publication date: 9-Jan-2024
https://dl.acm.org/doi/10.1145/3636501.3636945
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents