{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:48:59Z","timestamp":1775868539729,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":22,"publisher":"ACM","license":[{"start":{"date-parts":[[2012,1,25]],"date-time":"2012-01-25T00:00:00Z","timestamp":1327449600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2012,1,25]]},"DOI":"10.1145\/2103656.2103690","type":"proceedings-article","created":{"date-parts":[[2012,1,24]],"date-time":"2012-01-24T11:47:19Z","timestamp":1327405639000},"page":"273-284","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Static and user-extensible proof checking"],"prefix":"10.1145","author":[{"given":"Antonis","family":"Stampoulis","sequence":"first","affiliation":[{"name":"Yale University, New Haven, CT, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhong","family":"Shao","sequence":"additional","affiliation":[{"name":"Yale University, New Haven, CT, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2012,1,25]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Handbook of Automated Reasoning","author":"Barendregt H.P.","year":"1999","unstructured":"H.P. Barendregt and H. Geuvers . Proof-assistants using dependent type systems . In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning . Elsevier Sci . Pub. B.V., 1999 . H.P. Barendregt and H. Geuvers. Proof-assistants using dependent type systems. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Sci. Pub. B.V., 1999."},{"key":"e_1_3_2_2_2_1","volume-title":"The Coq proof assistant reference manual (version 8.3)","author":"Barras B.","year":"2010","unstructured":"B. Barras , S. Boutin , C. Cornes , J. Courant , Y. Coscoy , D. Delahaye , D. de Rauglaudre , J.C. Filli\u00e2tre , E. Gim\u00e9nez , H. Herbelin , The Coq proof assistant reference manual (version 8.3) , 2010 . B. Barras, S. Boutin, C. Cornes, J. Courant, Y. Coscoy, D. Delahaye, D. de Rauglaudre, J.C. Filli\u00e2tre, E. Gim\u00e9nez, H. Herbelin, et al. The Coq proof assistant reference manual (version 8.3), 2010."},{"key":"e_1_3_2_2_3_1","first-page":"671","volume-title":"Rewriting Techniques and Applications","author":"Blanqui F.","year":"1999","unstructured":"F. Blanqui , J.P. Jouannaud , and M. Okada . The calculus of algebraic constructions . In Rewriting Techniques and Applications , pages 671 -- 671 . Springer , 1999 . F. Blanqui, J.P. Jouannaud, and M. Okada. The calculus of algebraic constructions. In Rewriting Techniques and Applications, pages 671--671. Springer, 1999."},{"key":"e_1_3_2_2_4_1","volume-title":"A calculus of congruent constructions. Unpublished draft","author":"Blanqui F.","year":"2005","unstructured":"F. Blanqui , J.P. Jouannaud , and P.Y. Strub . A calculus of congruent constructions. Unpublished draft , 2005 . F. Blanqui, J.P. Jouannaud, and P.Y. Strub. A calculus of congruent constructions. Unpublished draft, 2005."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/645869.668533"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_2_7_1","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable R.L.","year":"1986","unstructured":"R.L. Constable , S.F. Allen , H.M. Bromley , W.R. Cleaveland , J.F. Cremer , R.W. Harper , D.J. Howe , T.B. Knoblock , N.P. Mendler , P. Panangaden , Implementing Mathematics with the Nuprl Proof Development System . Prentice-Hall , NJ , 1986 . R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, NJ, 1986."},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237788"},{"issue":"11","key":"e_1_3_2_2_9_1","first-page":"1382","article-title":"Formal proof--the four-color theorem","volume":"55","author":"Gonthier G.","year":"2008","unstructured":"G. Gonthier . Formal proof--the four-color theorem . Notices of the AMS , 55 ( 11 ): 1382 -- 1393 , 2008 . G. Gonthier. Formal proof--the four-color theorem. Notices of the AMS, 55 (11): 1382--1393, 2008.","journal-title":"Notices of the AMS"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034798"},{"key":"e_1_3_2_2_11_1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"A tutorial introduction","author":"Harrison J.","year":"1996","unstructured":"J. Harrison . HOL Light : A tutorial introduction . Lecture Notes in Computer Science , pages 265 -- 269 , 1996 . J. Harrison. HOL Light: A tutorial introduction. Lecture Notes in Computer Science, pages 265--269, 1996."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_14_1","series-title":"LNCS","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL : A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L.C. Paulson , and M. Wenzel . Isabelle\/HOL : A Proof Assistant for Higher-Order Logic , volume 2283 of LNCS , 2002 . T. Nipkow, L.C. Paulson, and M. Wenzel. Isabelle\/HOL : A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS, 2002."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389469"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792887"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.19"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1789277.1789293"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863591"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103690"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1887459.1887501"}],"event":{"name":"POPL '12: The 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Philadelphia PA USA","acronym":"POPL '12","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2103656.2103690","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2103656.2103690","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:06:21Z","timestamp":1750226781000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2103656.2103690"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,1,25]]},"references-count":22,"alternative-id":["10.1145\/2103656.2103690","10.1145\/2103656"],"URL":"https:\/\/doi.org\/10.1145\/2103656.2103690","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2103621.2103690","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2012,1,25]]},"assertion":[{"value":"2012-01-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}