{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:26:06Z","timestamp":1750220766350,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2020,1,20]],"date-time":"2020-01-20T00:00:00Z","timestamp":1579478400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001502","name":"Department of Atomic Energy, Government of India","doi-asserted-by":"publisher","award":["12-R&D-TFR-5.01-0500"],"award-info":[{"award-number":["12-R&D-TFR-5.01-0500"]}],"id":[{"id":"10.13039\/501100001502","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2020,1,20]]},"DOI":"10.1145\/3372885.3373819","type":"proceedings-article","created":{"date-parts":[[2020,1,22]],"date-time":"2020-01-22T13:09:33Z","timestamp":1579698573000},"page":"313-324","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["A constructive formalization of the weak perfect graph theorem"],"prefix":"10.1145","author":[{"given":"Abhishek Kr","family":"Singh","sequence":"first","affiliation":[{"name":"Tata Institute of Fundamental Research, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raja","family":"Natarajan","sequence":"additional","affiliation":[{"name":"Tata Institute of Fundamental Research, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,1,22]]},"reference":[{"volume-title":"Perfect Graphs and the Perfect Graph Theorems. Master\u2019s thesis","author":"Ballen Peter","key":"e_1_3_2_1_1_1","unstructured":"Peter Ballen . 2014. Perfect Graphs and the Perfect Graph Theorems. Master\u2019s thesis . Swarthmore College . peterballen.com Peter Ballen. 2014. Perfect Graphs and the Perfect Graph Theorems. Master\u2019s thesis. Swarthmore College. peterballen.com"},{"volume-title":"A formal theory of undirected graphs in higher-order logc","author":"Chou Ching-Tsun","key":"e_1_3_2_1_2_1","unstructured":"Ching-Tsun Chou . 1994. A formal theory of undirected graphs in higher-order logc . In Higher Order Logic Theorem Proving and Its Applications, Thomas F. Melham and Juanito Camilleri (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg , 144\u2013157. Ching-Tsun Chou. 1994. A formal theory of undirected graphs in higher-order logc. In Higher Order Logic Theorem Proving and Its Applications, Thomas F. Melham and Juanito Camilleri (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 144\u2013157."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.4007\/annals.2006.164.51"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Christian Doczkal Guillaume Combette and Damien Pous. 2018. A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. In Interactive Theorem Proving Jeremy Avigad and Assia Mahboubi (Eds.). 178\u2013195.  Christian Doczkal Guillaume Combette and Damien Pous. 2018. A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. In Interactive Theorem Proving Jeremy Avigad and Assia Mahboubi (Eds.). 178\u2013195.","DOI":"10.1007\/978-3-319-94821-8_11"},{"key":"e_1_3_2_1_5_1","volume-title":"First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (Lecture Notes in Computer Science), Matt Kaufmann and Lawrence C. Paulson (Eds.)","volume":"6172","author":"Dufourd Jean-Fran\u00e7ois","year":"2010","unstructured":"Jean-Fran\u00e7ois Dufourd and Yves Bertot . 2010 . Formal Study of Plane Delaunay Triangulation. In Interactive Theorem Proving , First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (Lecture Notes in Computer Science), Matt Kaufmann and Lawrence C. Paulson (Eds.) , Vol. 6172 . Springer, 211\u2013226. Jean-Fran\u00e7ois Dufourd and Yves Bertot. 2010. Formal Study of Plane Delaunay Triangulation. In Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings (Lecture Notes in Computer Science), Matt Kaufmann and Lawrence C. Paulson (Eds.), Vol. 6172. Springer, 211\u2013226."},{"key":"e_1_3_2_1_6_1","unstructured":"Coq formalization. 2019. https:\/\/github.com\/Abhishek-TIFR\/wpgt  Coq formalization. 2019. https:\/\/github.com\/Abhishek-TIFR\/wpgt"},{"key":"e_1_3_2_1_7_1","volume-title":"Johnson","author":"Garey Michael R.","year":"1990","unstructured":"Michael R. Garey and David S . Johnson . 1990 . Computers and Intractability; A Guide to the Theory of NP-Completeness. W. H. Freeman & amp; Co., New York, NY, USA. Michael R. Garey and David S. Johnson. 1990. Computers and Intractability; A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York, NY, USA."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87827-8_28"},{"key":"e_1_3_2_1_9_1","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier Georges","year":"2010","unstructured":"Georges Gonthier and Assia Mahboubi . 2010 . An introduction to small scale reflection in Coq . Journal of Formalized Reasoning 3 , 2 (2010), 95 \u2013 152 . https:\/\/hal.inria.fr\/inria-00515548 Georges Gonthier and Assia Mahboubi. 2010. An introduction to small scale reflection in Coq. Journal of Formalized Reasoning 3, 2 (2010), 95\u2013152. https:\/\/hal.inria.fr\/inria-00515548","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jctb.2012.06.001"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(72)90006-4"},{"key":"e_1_3_2_1_12_1","unstructured":"The Coq development team. 2016. The Coq proof assistant reference manual. Version 8.5.  The Coq development team. 2016. The Coq proof assistant reference manual. Version 8.5."},{"key":"e_1_3_2_1_13_1","volume-title":"Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (Lecture Notes in Computer Science), Ulrich Furbach and Natarajan Shankar (Eds.)","volume":"4130","author":"Nipkow Tobias","year":"2006","unstructured":"Tobias Nipkow , Gertrud Bauer , and Paula Schultz . 2006 . Flyspeck I: Tame Graphs. In Automated Reasoning , Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (Lecture Notes in Computer Science), Ulrich Furbach and Natarajan Shankar (Eds.) , Vol. 4130 . Springer, 21\u201335. Tobias Nipkow, Gertrud Bauer, and Paula Schultz. 2006. Flyspeck I: Tame Graphs. In Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings (Lecture Notes in Computer Science), Ulrich Furbach and Natarajan Shankar (Eds.), Vol. 4130. Springer, 21\u201335."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0183-z"},{"key":"e_1_3_2_1_15_1","volume-title":"ICLA 2019, Delhi, India, March 1-5, 2019, Proceedings. 183\u2013194","author":"Singh Abhishek Kr","year":"2019","unstructured":"Abhishek Kr Singh and Raja Natarajan . 2019 . Towards a Constructive Formalization of Perfect Graph Theorems. In Logic and Its Applications - 8th Indian Conference , ICLA 2019, Delhi, India, March 1-5, 2019, Proceedings. 183\u2013194 . Abhishek Kr Singh and Raja Natarajan. 2019. Towards a Constructive Formalization of Perfect Graph Theorems. In Logic and Its Applications - 8th Indian Conference, ICLA 2019, Delhi, India, March 1-5, 2019, Proceedings. 183\u2013194."},{"key":"e_1_3_2_1_16_1","volume-title":"Perfect graphs: a survey. ArXiv e-prints (Jan","author":"Trotignon N.","year":"2013","unstructured":"N. Trotignon . 2013. Perfect graphs: a survey. ArXiv e-prints (Jan . 2013 ). arXiv: math.CO\/1301.5149 N. Trotignon. 2013. Perfect graphs: a survey. ArXiv e-prints (Jan. 2013). arXiv: math.CO\/1301.5149"}],"event":{"name":"POPL '20: 47th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"New Orleans LA USA","acronym":"POPL '20"},"container-title":["Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373819","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3372885.3373819","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:09Z","timestamp":1750200069000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3372885.3373819"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,1,20]]},"references-count":16,"alternative-id":["10.1145\/3372885.3373819","10.1145\/3372885"],"URL":"https:\/\/doi.org\/10.1145\/3372885.3373819","relation":{},"subject":[],"published":{"date-parts":[[2020,1,20]]},"assertion":[{"value":"2020-01-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}