{"entities":{"Q5408420":{"pageid":7437994,"ns":120,"title":"Item:Q5408420","lastrevid":33016375,"modified":"2024-03-20T01:32:06Z","type":"item","id":"Q5408420","labels":{"en":{"language":"en","value":"30 years of research and development around Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6282426"}},"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":"Q5408420$87F98A5D-470A-4526-AE39-27A65551FEB5","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"85adca4e71481bfa5a7fcf07d10e1ca53ec491b8","datavalue":{"value":{"text":"30 years of research and development around Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5408420$359372FC-A686-4F0B-AEAF-E3B69F4904CD","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4e40317e20ea203846605a7bdb15df0e3dd079ac","datavalue":{"value":"1284.68517","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408420$783F14F8-34AB-4BDC-A06D-8E05844264F5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7fd4fe19a484addd2768d1febced285449fa1eba","datavalue":{"value":"10.1145/2535838.2537848","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408420$AFFB50AB-82C6-4E21-97A6-05979D54DB71","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4f9facad47142ae6aca78e42226d987a134e9bf3","datavalue":{"value":{"entity-type":"item","numeric-id":789175,"id":"Q789175"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408420$3EA23541-BF04-4804-AEEE-97B9015FC253","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"efed21e9824a359c8d3282e3ffda49b99e5e2e03","datavalue":{"value":{"entity-type":"item","numeric-id":636370,"id":"Q636370"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408420$47A09B0C-33B2-4832-918B-5A5976C6F472","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"640f3283bf4ebaf19f5992b18fbb1bf0f8463c2b","datavalue":{"value":{"entity-type":"item","numeric-id":5408394,"id":"Q5408394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5408420$27139217-7CA5-48ED-9271-C934504E5FF1","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d29d162184913e14034b04455ad3f441d2a1856b","datavalue":{"value":{"time":"+2014-04-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5408420$D549E262-B986-4882-86BE-880CDD02CEDA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408420$BF735232-EF99-49E8-A069-F67DDB096936","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"540259e42205310d3310d3dad9dbe9ae50303b84","datavalue":{"value":"68-03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408420$C8041ADF-BAB8-4AD5-A211-2EA27FE63DE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408420$D046CE18-72CE-49E8-A8EF-71D9DB9EC207","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408420$2B0BE55E-29D2-4A43-AE4D-09AE0833F2C8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b059ac0ab403e472713e76785c3636b574de11fe","datavalue":{"value":"6282426","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408420$27B80E3F-D536-4560-B053-D4AEF424AD2D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8ee22a16b68ff7690ced49d39b0f7a8a6db96b60","datavalue":{"value":"calculus of inductive constructions","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408420$09925F25-A361-403C-9524-838E791DEEB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"736332c97b41fa000c78786243a5eba2232db4aa","datavalue":{"value":"certified programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408420$EFAFAE88-6616-4FDC-B6F3-79F1630440E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408420$510DEE35-347E-4331-A011-0974AED5CD99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"658126897c7f6bf3db78fea48b2876524c1d8c9e","datavalue":{"value":"formalization of mathematics","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408420$E18C71BD-BB64-44CA-8697-7CCA363A5582","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408420$74DAAD40-7E5D-441D-AB83-E379CA446CAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q5408420$93188B9F-712A-4F7D-8B04-1A5F80B7E38B","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":"Q5408420$3D46E679-CCAA-42CA-A22E-392532CA9B45","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ac28c81980973ababfa2c75e67c494a9e556c6b5","datavalue":{"value":"https://doi.org/10.1145/2535838.2537848","type":"string"},"datatype":"url"},"type":"statement","id":"Q5408420$DC40D934-8EBE-451E-8CF5-5F9A1FE6B88D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9c01ae573405ecf2054b3fb9a2bcb5d627c2f843","datavalue":{"value":"W2055815710","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5408420$E02870F1-3976-4DD7-AF57-0A0B57D0E92A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5408420","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5408420"}}}}}