{"entities":{"Q6083698":{"pageid":13218005,"ns":120,"title":"Item:Q6083698","lastrevid":98649743,"modified":"2026-06-05T18:09:27Z","type":"item","id":"Q6083698","labels":{"en":{"language":"en","value":"Developing certified programs in the system Coq the program tactic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7774599"}},"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":"Q6083698$3AA0740E-D4B2-4797-8D52-B4456D8EC872","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"de9cb8f10abc1d9bccb683bc8dba28ca17d45c63","datavalue":{"value":{"text":"Developing certified programs in the system Coq the program tactic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6083698$76E0B815-5DB0-4CBB-86BD-0746FFF9CDEE","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"9a07d6f77fad920ced1afc10b15ae7e079d03455","datavalue":{"value":"1527.68134","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083698$28ACC3AA-E4FF-4F70-B9C7-8E0ED1268E2D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"56fc17c510d207134df45f2c08017dbd49f7a59b","datavalue":{"value":"10.1007/3-540-58085-9_81","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083698$6B719109-8ED9-43D8-9838-5B31D43C399D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ed302b6d3ad54d111aa2cd08ba233962d0e45f85","datavalue":{"value":{"entity-type":"item","numeric-id":2385445,"id":"Q2385445"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083698$9D18B0E7-0F29-48D5-BBE3-FE61AA494BD0","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083698$BF94539C-004B-4EFB-8000-A50EA3966C59","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"80837e4f107d88dc61f75b08f8b7aa1a590aa151","datavalue":{"value":{"time":"+2023-12-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6083698$E0E5221F-2E81-4A2D-8F92-EB89AD5F9ECA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083698$467BAD54-9104-4391-971B-0597C2E295C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083698$885CE6F0-D7C9-4D15-9C0D-A69D35997AAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083698$03217A89-F5DB-4723-A537-4220D5D4F9BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083698$58F3B578-D996-4ED9-A485-08E0935F5AA3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6aaeba8e495c56f99a7363363a0ac7801fef8dd8","datavalue":{"value":"7774599","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083698$A054701C-4BD7-4886-9809-87C830078080","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":"Q6083698$51CB3E4F-5125-41C3-8FDC-2C99FCC4B9EF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec2b382496704c69d4ddd122d1fda39bebf3ce71","datavalue":{"value":{"entity-type":"item","numeric-id":4939699,"id":"Q4939699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083698$877BB1A4-3A62-4825-94A3-EE656A2E491C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9ac899433a8e17454dc938a2d4fc8f05db348c5e","datavalue":{"value":{"entity-type":"item","numeric-id":4871733,"id":"Q4871733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083698$48B43645-549A-457D-97D7-1A121A93FD2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"774c18fd2b844ce5d75610805893e277658a480f","datavalue":{"value":{"entity-type":"item","numeric-id":4276174,"id":"Q4276174"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083698$303E6966-562C-4807-B8CB-BFA9DE043BBE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3ed33d75210f4b470fc995229f8d6e408696f04","datavalue":{"value":{"entity-type":"item","numeric-id":3922646,"id":"Q3922646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083698$82A4EEB7-1775-4D0E-B1A3-18B790E9CAED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9579a4ebc8fc362938d3ee4c1626b4dbb8862f2","datavalue":{"value":{"entity-type":"item","numeric-id":4281483,"id":"Q4281483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083698$61BF76BA-67C4-4C5A-8C40-8C4903D97118","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"82af13d5271451c4bb72d7b055064b56ff1b2fb5","datavalue":{"value":{"entity-type":"item","numeric-id":1322847,"id":"Q1322847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083698$A7A51EB3-9A42-4435-B4B9-05373719B534","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":"5d300b73e2dab7ad03accf32d23af0ef1a29a890","datavalue":{"value":{"amount":"+0.8557501435279846","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":"Q6083698$0D3A87CB-A6F8-4C8D-933F-B6109AA3D10B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"714e15e5a2ba4fff06e9121fed38d3236869a4fd","datavalue":{"value":{"entity-type":"item","numeric-id":1267035,"id":"Q1267035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d4d94f3cd279ab994e9a40839196ee9b34a1d294","datavalue":{"value":{"amount":"+0.8368532061576843","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":"Q6083698$21632336-93B8-4F67-9ACE-FFD76D315E39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"126be7296d6b7110e1000144e41a4b9d8fcc6ece","datavalue":{"value":{"entity-type":"item","numeric-id":4435471,"id":"Q4435471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce6234b8b7bb384e9124b3a91404b9a3c0e9b369","datavalue":{"value":{"amount":"+0.8130396008491516","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":"Q6083698$DB067C17-E16A-45A7-84B1-3985378B224D","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":"bffded606541e01f9caf488a71213014c1ac9cee","datavalue":{"value":{"amount":"+0.7855918407440186","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":"Q6083698$9278D605-FB00-4E62-875A-8AAAD4468F15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81235c4d3f4c66b6911717e8cbf43cd34a5bdfea","datavalue":{"value":{"entity-type":"item","numeric-id":912594,"id":"Q912594"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b2b0e8a02369169c447b5a938a453a1a121b56f","datavalue":{"value":{"amount":"+0.7843024134635925","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":"Q6083698$6C3A782F-E1C3-4C9C-BA29-EE55607FDBFF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Developing certified programs in the system Coq the program tactic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Developing_certified_programs_in_the_system_Coq_the_program_tactic"}}}}}