{"entities":{"Q6854558":{"pageid":20623990,"ns":120,"title":"Item:Q6854558","lastrevid":101349899,"modified":"2026-06-06T00:40:14Z","type":"item","id":"Q6854558","labels":{"en":{"language":"en","value":"Correct and complete type checking and certified erasure for \\textsc{Coq}, in \\textsc{Coq}"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8162999"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$B5363568-2878-49D2-A220-E2C7DBE67FCB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cf28c799de57afb91ee3e1f3d4f1825190eddaae","datavalue":{"value":{"text":"Correct and complete type checking and certified erasure for \\textsc{Coq}, in \\textsc{Coq}","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6854558$DA2200CF-E13D-40A4-BD34-5A3B68A4C59D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f9cd2bf271f105ca8836135e5980d9705343d11d","datavalue":{"value":"10.1145/3706056","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854558$3AE14EB1-5E28-4BBB-9CF7-A308C364C934","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"a9414558f268ee594724569b856f23c96f190f01","datavalue":{"value":{"entity-type":"item","numeric-id":1791139,"id":"Q1791139"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$9856780E-A59B-4134-8759-EC36C2138E25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c7e7e54e22918a5af75f6588d5e6c4a6d7874c28","datavalue":{"value":{"entity-type":"item","numeric-id":1687734,"id":"Q1687734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$E3C2B681-FAA5-46E1-A40F-12E5CF3C1ADF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e4ef8f5dfcdcdf632810bd8e30618f6b62925045","datavalue":{"value":{"entity-type":"item","numeric-id":6099614,"id":"Q6099614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$6A10C5BA-71A0-4DA9-99E4-1BC8283BE0AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7f88ed56af083154f11eab025a065bb3de45e3c2","datavalue":{"value":{"entity-type":"item","numeric-id":4271956,"id":"Q4271956"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$1C9D5DAC-2973-434F-82A3-B5FB632E1469","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1f7519cb4a1f2077b5761baeaf0abc45060a0b93","datavalue":{"value":{"entity-type":"item","numeric-id":636302,"id":"Q636302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$15E501E9-0A13-4010-8C2E-0392F9A07E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"782705f79a6a25f37d278cde3e4e69f417039f3e","datavalue":{"value":{"entity-type":"item","numeric-id":2209541,"id":"Q2209541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$8382B6FB-277B-45F7-A6F7-33252F848BA3","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f12bfc80fe4a431c556e028f5134a217234a7cc4","datavalue":{"value":{"entity-type":"item","numeric-id":63915,"id":"Q63915"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$82825BAF-6D02-4391-B929-7E6B3FD2F31C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"23f7bc78d27ce33f5d6c9d48966ef81d2c43df8b","datavalue":{"value":{"time":"+2026-02-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6854558$163F91C9-3B5A-4F67-AD24-822722BE78DC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854558$AD8CD97C-0934-4D2D-BB8E-89E428F55557","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"75950e9bc1e99f71747a8af8847097c4bdcedb6a","datavalue":{"value":"8162999","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6854558$449EA181-0782-4B84-B86E-A1DEC6532DB9","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$4D0867B1-7ACB-4D15-9BF0-6CE8FF0620FD","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854558$FA5EE23E-1A3F-4CE2-B62F-AF28E3E126C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c41e0dc982d673770a568fd6d468deb1e59e355b","datavalue":{"value":"type checker","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854558$826D7F79-3790-4F5D-A4F2-4D23B361773F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"58d5c9c0cf89b4b4891f5c481837b69838035e8a","datavalue":{"value":"certification","type":"string"},"datatype":"string"},"type":"statement","id":"Q6854558$AC7DA223-6ABF-482D-B260-9B14DA62B7FF","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$67784B25-9A23-4A36-B517-5CA0EE01B178","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5249c80fcd11fa0612fb7dd29644b8dc29907a14","datavalue":{"value":{"entity-type":"item","numeric-id":4939690,"id":"Q4939690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$62600FAE-624C-4F33-AC0C-23C25E5F3FAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"40baf4bdceb7bc43f795fddb529b32cd0b1cc67e","datavalue":{"value":{"entity-type":"item","numeric-id":5466528,"id":"Q5466528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$4607BEC2-A055-418F-BBE2-7FC4BD7FAD2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"57ea5885832b9f867e6bed74c7137f05eec86479","datavalue":{"value":{"entity-type":"item","numeric-id":2931780,"id":"Q2931780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$CEC54D47-852F-477A-84F6-70DD942FE55B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"457ec7d32f0f86f3bbf301599db4ae5da346089d","datavalue":{"value":{"entity-type":"item","numeric-id":6572534,"id":"Q6572534"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$538E86D6-82FC-471D-BBF0-01AD63B1AE58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67cec2a0d4cf53a41e2611922340c200ac53fb76","datavalue":{"value":{"entity-type":"item","numeric-id":1791140,"id":"Q1791140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$6AFF779F-2C5B-4022-9F07-38762B6FC751","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c9864722e1120856743b1e5eb3761fb8bcb430e4","datavalue":{"value":{"entity-type":"item","numeric-id":2879241,"id":"Q2879241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$CFBD8A45-2CA3-4921-813A-1108CC9A49E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81543691b4e263c5797e859d5b3ba26c0a4ed4e1","datavalue":{"value":{"entity-type":"item","numeric-id":5101927,"id":"Q5101927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$6B9D377C-F843-4B70-97BE-08AB5912B003","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f804ba9bd933e99538ba26edc67730d9ee308ef","datavalue":{"value":{"entity-type":"item","numeric-id":5458373,"id":"Q5458373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$2323008C-AF29-4C08-8933-2A0A00C8FCE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"acbf68a35efd53fa46006569e2fcabd7e445489d","datavalue":{"value":{"entity-type":"item","numeric-id":4962211,"id":"Q4962211"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$17DE676C-20E0-4114-9182-599E6FEC2E94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"623d2e57b8048f48b862896a58bf8da52ad9d8d6","datavalue":{"value":{"entity-type":"item","numeric-id":2123048,"id":"Q2123048"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$BE97A901-9DA6-4962-A024-F296ED62C269","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$64328575-2038-4B83-8C2B-3FA0004787F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"541bc36e9357802534d1e52134710ec758d76fb7","datavalue":{"value":{"entity-type":"item","numeric-id":5753923,"id":"Q5753923"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$F35BF2D8-3250-4243-A217-DDD894479D23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5e6e84dc7d2442795960d241851cf13bc84741e4","datavalue":{"value":{"entity-type":"item","numeric-id":1412830,"id":"Q1412830"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$D9BB8ECD-5FA8-4B1D-A394-CD8C98C8DEA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"659834f1596059b45ef2192e187dd9ba3dcf6dd0","datavalue":{"value":{"entity-type":"item","numeric-id":5875425,"id":"Q5875425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$5B17775D-8E66-451F-AFC2-672828B79B65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8b276a4466d3408aebe4dbddd64d84bba4e9bbb3","datavalue":{"value":{"entity-type":"item","numeric-id":5875426,"id":"Q5875426"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$181559C1-A863-4609-9C96-562A74F21E3C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c3c69fa2672b8fa81e2d2be45ac3f1049ef642d","datavalue":{"value":{"entity-type":"item","numeric-id":5277716,"id":"Q5277716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$32473C0F-2A6C-4887-B50B-A5856A303B93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca9b21e92d1e385b1aa703cba49bf61d8d21f05a","datavalue":{"value":{"entity-type":"item","numeric-id":1177937,"id":"Q1177937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$A70CF4FD-DA9A-4DBF-A97E-4C9BF574A9AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78757e9c4e37a9fa53a10705a27e9c8cff416b63","datavalue":{"value":{"entity-type":"item","numeric-id":2324018,"id":"Q2324018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$BDBFE2FB-BDDC-4EB3-8734-94EE85B6E336","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d623a8e65d7930da0f4edbbd56cfd23f3252fedf","datavalue":{"value":{"entity-type":"item","numeric-id":3024841,"id":"Q3024841"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$13C7973E-A082-47AD-9049-3F5172ED05EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8859bdb6b4bc274ef2c6f9c1117c4e5c707d7424","datavalue":{"value":{"entity-type":"item","numeric-id":3224695,"id":"Q3224695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$A200EF30-6B61-4E0D-B150-1FFB9D13CE5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bcd794e9602f713eb2dd357e2a648e63a03d08e8","datavalue":{"value":{"entity-type":"item","numeric-id":6099615,"id":"Q6099615"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$DDB49FD6-0716-4F64-A1DC-7E19FFDD19E5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2f77790f3de0e7a5198a8f1c64a8023dd2bee09","datavalue":{"value":{"entity-type":"item","numeric-id":5348912,"id":"Q5348912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$D6D778C6-F44E-4419-987C-1FE8BFE82659","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bb1812a83c3a4aee25d6a67b2527c143aea9ae4","datavalue":{"value":{"entity-type":"item","numeric-id":4435471,"id":"Q4435471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$5A8A016E-A990-4FE0-A1FA-A626C6715571","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$18A96032-6FD5-41EF-91EB-B025763A32FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d91a6fc5a255cbadfa617ce94146193166c4f9ed","datavalue":{"value":{"entity-type":"item","numeric-id":4247306,"id":"Q4247306"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$871DE5CE-8EC7-4456-8533-7EC3B04ACEB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3893e24895c818d766b4ac601e2292c1956a8e2a","datavalue":{"value":{"entity-type":"item","numeric-id":4819653,"id":"Q4819653"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$95411E9B-D737-428C-A73D-7AC1A38E97A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"227fe77aa9bac83e88e8a7622effb8e94001c51a","datavalue":{"value":{"entity-type":"item","numeric-id":2875232,"id":"Q2875232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$3F96C178-06E7-44FB-B4FC-D499BCA494ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d8f88db4db4ff3067bd759c8807bea327b3eccfd","datavalue":{"value":{"entity-type":"item","numeric-id":1094421,"id":"Q1094421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$C9517D9F-F90B-47EF-8CFC-380BD0191691","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"880dd2d891bee7d89376be3d87fc756a3f8aa32d","datavalue":{"value":{"entity-type":"item","numeric-id":5144660,"id":"Q5144660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$DC9B98A0-3D48-4C8E-8AAF-67D7ACC764F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2788a32b1e668b3e184e8bfcb48f92a0fa8df1e","datavalue":{"value":{"entity-type":"item","numeric-id":4983210,"id":"Q4983210"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$091E768F-3D9B-45EE-AAF6-395826D52A2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ccdfc6c2a229e09846d7ccb887c26192d20ce0f8","datavalue":{"value":{"entity-type":"item","numeric-id":2945649,"id":"Q2945649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$10743508-02D7-4719-B179-C96E6B05DB14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"681f6b991823ef1eb2ae5a0dc4952d80f163b9df","datavalue":{"value":{"entity-type":"item","numeric-id":2844696,"id":"Q2844696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$5FDF8F6E-166D-4B5E-9324-574505427B2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ca5666f921e01dd97435dae76a72d1660a28c596","datavalue":{"value":{"entity-type":"item","numeric-id":2879272,"id":"Q2879272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$4F0A4E4F-D59D-4D6A-9286-1002EE342912","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c5e8926cf4c76489d22094514896f7168cc77887","datavalue":{"value":{"entity-type":"item","numeric-id":5903814,"id":"Q5903814"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$17E458AE-8029-4B4D-95D5-3A5D46B7178E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f6bf9de9e2014e93e277e777180ed630b8cc1b3","datavalue":{"value":{"entity-type":"item","numeric-id":5875441,"id":"Q5875441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$0A22D6DC-81A5-4078-B66D-8747A73BB354","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"980b703e2063f9bf90424e175cd7a7b4a6a1d2fc","datavalue":{"value":{"entity-type":"item","numeric-id":4993361,"id":"Q4993361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6854558$221A42C4-3960-4B62-AEDB-7B56B11A5CB4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6854558","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6854558"}}}}}