{"entities":{"Q4989018":{"pageid":7018595,"ns":120,"title":"Item:Q4989018","lastrevid":54004040,"modified":"2026-01-26T01:50:28Z","type":"item","id":"Q4989018","labels":{"en":{"language":"en","value":"A proof system for MSVL programs in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7350162"}},"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":"Q4989018$9677334C-B844-49F1-B2AD-F62C52AE7421","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"0e0fed912efb3092616e37bb89d830eea23d95c2","datavalue":{"value":{"text":"A Proof System for MSVL Programs in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4989018$45A6C603-DE0A-45E1-8148-6ADB3F319273","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"92e091d24aa4b8b3ad459906ff5c7d6229d480a9","datavalue":{"value":"1461.68058","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989018$AC10C5AA-AEE1-4EBA-AF19-3FB638FA6F0B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"35d9015a4b0926408b5bece8f4855b2baa86441e","datavalue":{"value":"10.1007/978-3-319-57708-1_8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989018$D08DA9F6-0D4B-4F30-9528-274765469011","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e7952e9949503a5ee5947448a642c19f945160c5","datavalue":{"value":{"entity-type":"item","numeric-id":3396968,"id":"Q3396968"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4989018$2A4C919F-A6AC-45A6-A142-E936F120F259","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"30d9aa89bda10e60a2b2b6e5c4297a8a726a7ab3","datavalue":{"value":{"entity-type":"item","numeric-id":247891,"id":"Q247891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4989018$38B5CD5C-091C-44DE-BB15-1E6A00496AD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"83e0c9ae8671e5f29856e35bbe5db8cbb2ecbb5c","datavalue":{"value":{"entity-type":"item","numeric-id":247888,"id":"Q247888"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4989018$44768723-2A1C-49F8-B7B4-82F7FA930712","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b63c8a7d27ac589b244a048d2f920a9e8c6bd330","datavalue":{"value":{"entity-type":"item","numeric-id":247892,"id":"Q247892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4989018$DE60A340-3ED0-4D69-81E3-644DBE9B985A","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"46c13b4ed20d7be55f678f5b2789c4af66377d94","datavalue":{"value":{"entity-type":"item","numeric-id":4989013,"id":"Q4989013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4989018$4A34C0B5-E7AD-418D-A6C8-6A366234DED9","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"211031a52806337129a1eef00df007a6622a5387","datavalue":{"value":{"time":"+2021-05-20T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4989018$BFC9C70C-45B8-4E97-BD94-AEE992095A1A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989018$2B420064-9B35-47F1-8E41-2A310F87CAF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989018$4C9E2011-B1B8-40EA-8DED-22CD2FCE3D3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989018$2660FCFE-110C-4E3F-A314-CF134D22BD6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989018$7B791183-E2A9-4DC2-B782-C2A78DEB1D90","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"59d50fe3b9e5d70ac15bdd18374094edc2ecbcbd","datavalue":{"value":"7350162","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989018$6EA74326-978E-485D-85F0-72BB0D900787","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"84e026c37b065e90ea6a0c462c4ada94e004527d","datavalue":{"value":"MSVL","type":"string"},"datatype":"string"},"type":"statement","id":"Q4989018$4C340D53-A3C1-4F01-829D-78E9E4F21C2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2087dc8eccfb57b61b26579b24f6230e971c84f2","datavalue":{"value":"semi-automatic proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q4989018$D0F6C711-84D9-4E7F-B34C-41A6D893516B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"73f877e2f1bc95df5bf8181b9880837b7bf0c2ee","datavalue":{"value":"interactive theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q4989018$FF2E6458-4A46-4FFA-84D5-B771CBD51CCB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q4989018$83018859-5E26-4398-916B-671C6C746485","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4989018$CC6C1490-F074-417C-B363-896CEFC5FFE5","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":"Q4989018$9A5E5D61-CA10-43A2-AA87-28A5DBCEDFD1","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2e0860e2686bdc13f52ac3c1e347225c772e9a61","datavalue":{"value":"https://doi.org/10.1007/978-3-319-57708-1_8","type":"string"},"datatype":"url"},"type":"statement","id":"Q4989018$611D0690-73B6-447E-91E9-A8FD4ACA49B9","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6a9d4036dddc37db29ad91a512ab80c4f3947f8f","datavalue":{"value":"W2606289262","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4989018$9C4ABBB1-B144-40C5-B6AB-89590DA0A42B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"77217dc2085b0609e7fd5b1db191a64d2ac5718c","datavalue":{"value":{"entity-type":"item","numeric-id":1322847,"id":"Q1322847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5606cdf501d1f1ca7b4f6d6f11d19ee7a712e02","datavalue":{"value":{"amount":"+0.7463904619216919","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4989018$B8C1B19F-3259-47A2-A28F-C23EB717FE11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d1bf37c15e48fc38e72aa136040f068ea21e0838","datavalue":{"value":{"entity-type":"item","numeric-id":5417200,"id":"Q5417200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d7d6c25faaa3efb3ba6b516d40779b952aaf7e1","datavalue":{"value":{"amount":"+0.7463903427124023","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4989018$0A415448-BED4-4C1E-8A1E-2DE88EDE305D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb9dddab88830bb73e5cc345e05c5edcc135ff3c","datavalue":{"value":{"entity-type":"item","numeric-id":3060195,"id":"Q3060195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ceab7dd2e480940003226e0f2bdecbedff63e3a","datavalue":{"value":{"amount":"+0.7240957021713257","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4989018$FA7BDAE4-1A5D-4B4D-9456-D5A3F0306694","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9a2566155239714c00e61ec0ef8651340a4fc288","datavalue":{"value":{"entity-type":"item","numeric-id":3400636,"id":"Q3400636"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50deb50ae65b1a05f55ff8234176b0f721468506","datavalue":{"value":{"amount":"+0.7211419939994812","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4989018$306C94E2-606B-4B48-B724-CC98A3F58506","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24cdcf48e2229f3526631ece2a3e1a80cc930fcc","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"430be1dd108619ca08996d90a24a998f10b69598","datavalue":{"value":{"amount":"+0.7193558812141418","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4989018$BA6E859C-C779-420C-A0C1-6A9B52583D30","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4989018","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4989018"}}}}}