{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:14:57Z","timestamp":1750306497688,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,18]],"date-time":"2016-01-18T00:00:00Z","timestamp":1453075200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P26201"],"award-info":[{"award-number":["P26201"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,18]]},"DOI":"10.1145\/2854065.2854070","type":"proceedings-article","created":{"date-parts":[[2016,1,12]],"date-time":"2016-01-12T13:18:57Z","timestamp":1452604737000},"page":"58-65","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Towards a Mizar environment for Isabelle: foundations and language"],"prefix":"10.1145","author":[{"given":"Cezary","family":"Kaliszyk","sequence":"first","affiliation":[{"name":"University of Innsbruck, Austria"}]},{"given":"Karol","family":"P\u0105k","sequence":"additional","affiliation":[{"name":"University of Bia\u0142ystok, Poland"}]},{"given":"Josef","family":"Urban","sequence":"additional","affiliation":[{"name":"Czech Technical University in Prague, Czech Republic"}]}],"member":"320","published-online":{"date-parts":[[2016,1,18]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"8th International Workshop","volume":"971","author":"Agerholm S.","year":"1995"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021966832558"},{"first-page":"531","volume-title":"IJCAI","author":"Davis M.","key":"e_1_3_2_1_3_1"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_9"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"crossref","unstructured":"J.\n       \n      Harrison\n    .\n      \n  \n   \n  A Mizar mode for HOL. In J. von Wright J. Grundy and J. Harrison editors Theorem Proving in Higher Order Logics: 9th International Conference TPHOLs\u201996 volume \n  1125\n   of \n  Lecture Notes in Computer Science pages 203\u2013\n  220 Turku Finland 1996\n  . \n  Springer-Verlag\n  .   J. Harrison. A Mizar mode for HOL. In J. von Wright J. Grundy and J. Harrison editors Theorem Proving in Higher Order Logics: 9th International Conference TPHOLs\u201996 volume 1125 of Lecture Notes in Computer Science pages 203\u2013220 Turku Finland 1996. Springer-Verlag.","DOI":"10.1007\/BFb0105406"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"J.\n       \n      Hurd\n    .\n      \n  \n   \n  The OpenTheory standard theory library. In M. G. Bobaru K. Havelund G. J. Holzmann and R. Joshi editors NASA Formal Methods volume \n  6617\n   of \n  LNCS pages 177\u2013\n  191\n  . Springer 2011.   J. Hurd. The OpenTheory standard theory library. In M. G. Bobaru K. Havelund G. J. Holzmann and R. Joshi editors NASA Formal Methods volume 6617 of LNCS pages 177\u2013191. Springer 2011.","DOI":"10.1007\/978-3-642-20398-5_14"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9271-4"},{"key":"e_1_3_2_1_8_1","first-page":"1","article-title":"On the rules of suppositions","author":"Ja\u015bkowski S.","year":"1934","journal-title":"Studia Logica"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_7"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9330-8"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_23"},{"first-page":"12","volume-title":"WDS Proceedings of Contributed Papers: Part I \u2013 Mathematics and Computer Sciences","author":"Kun\u02c7car O.","key":"e_1_3_2_1_12_1"},{"key":"e_1_3_2_1_13_1","first-page":"3","article-title":"Mizar: the first 30 years","volume":"4","author":"Matuszewski R.","year":"2005","journal-title":"Mechanized Mathematics and Its Applications"},{"key":"e_1_3_2_1_14_1","first-page":"74","volume-title":"Workshop on Verification in New Orientations","author":"Merz S.","year":"1995"},{"volume-title":"Computer Reconstruction of the Body of Mathematics","year":"2009","author":"Naumowicz A.","key":"e_1_3_2_1_15_1"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11921240_19"},{"key":"e_1_3_2_1_17_1","volume-title":"Intelligent Computer Mathematics - International Conference, CICM","volume":"9150","author":"Obua S.","year":"2015"},{"key":"e_1_3_2_1_18_1","first-page":"386","volume-title":"Logic and Computer Science (1990","author":"Paulson L. C.","year":"1990"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00881873"},{"key":"e_1_3_2_1_20_1","volume-title":"The 8th International Workshop on the Implementation of Logics, IWIL 2010","volume":"2","author":"Paulson L. C.","year":"2010"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1080\/014453499298165"},{"key":"e_1_3_2_1_22_1","first-page":"251","volume-title":"International Conference on Automated Deduction (CADE","volume":"814","year":"1994"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129512000424"},{"key":"e_1_3_2_1_24_1","unstructured":". URL http:\/\/dx.doi.org\/10.1017\/ S0960129512000424.  . URL http:\/\/dx.doi.org\/10.1017\/ S0960129512000424."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/41391.41394"},{"issue":"2","key":"e_1_3_2_1_26_1","first-page":"111","volume":"15","author":"Schulz S.","year":"2002","journal-title":"AI Commun."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_7"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.4064\/fm-30-1-68-89"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0218213006002588"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-006-9032-3"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-008-0053-7"},{"key":"e_1_3_2_1_32_1","volume-title":"12th International Conference, TPHOLs\u201999","volume":"1690","author":"Wenzel M.","year":"1999"},{"key":"e_1_3_2_1_33_1","unstructured":"M. Wenzel. The Isabelle\/Isar reference manual 2015.  M. Wenzel. The Isabelle\/Isar reference manual 2015."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"e_1_3_2_1_35_1","unstructured":"F. Wiedijk. CHECKER - notes on the basic inference step in Mizar. available at http:\/\/www.cs.kun.nl\/\u223cfreek\/mizar\/by.dvi 2000. URL http:\/\/www.cs.kun.nl\/~freek\/mizar\/by.dvi.  F. Wiedijk. CHECKER - notes on the basic inference step in Mizar. available at http:\/\/www.cs.kun.nl\/\u223cfreek\/mizar\/by.dvi 2000. URL http:\/\/www.cs.kun.nl\/~freek\/mizar\/by.dvi."}],"event":{"name":"CPP 2016: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"St. Petersburg FL USA","acronym":"CPP 2016"},"container-title":["Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854070","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2854065.2854070","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:46Z","timestamp":1750225726000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854070"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,18]]},"references-count":35,"alternative-id":["10.1145\/2854065.2854070","10.1145\/2854065"],"URL":"https:\/\/doi.org\/10.1145\/2854065.2854070","relation":{},"subject":[],"published":{"date-parts":[[2016,1,18]]},"assertion":[{"value":"2016-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}