A Constructive Formalization of the Weak Perfect Graph Theorem
summary
Presents a constructive, machine-checked formalization of the Weak Perfect Graph Theorem using the Coq proof assistant and its Mathematical Components library. Covers the formal development of graph-theoretic results needed for the theorem and how constructive methods were used to encode and prove the theorem within Coq.
AI-written summary · about
related talks
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
36mMcTT: Building A Correct-By-Construction Proof Checker For Martin-Loef Type Theory
01h 34mFormal Logic Undressed
31mA Coq Library of Undecidable Problems
01h 03mVerifying Dependent Type-checkers
29mCertifying Complexity Analysis
21mBlack-box Constructive Proofs are Unavoidable