{"entities":{"Q6535845":{"pageid":14146988,"ns":120,"title":"Item:Q6535845","lastrevid":55593655,"modified":"2026-02-17T19:24:55Z","type":"item","id":"Q6535845","labels":{"en":{"language":"en","value":"A Coq implementation of the program algebra in Jifeng He's new roadmap for linking theories of programming"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7810663"}},"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":"Q6535845$833FE1F7-3C16-4F3D-B1EA-5205EE5057D2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8fb5d573b6852c4b293d5f2d45c4c2e2a3e7df97","datavalue":{"value":{"text":"A Coq implementation of the program algebra in Jifeng He's new roadmap for linking theories of programming","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6535845$FFB892EF-79AF-4945-BF0E-364C190FCC28","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6c753e32ec3aa5c4f27d990e4e3c5b5fad578d7b","datavalue":{"value":"1547.68129","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535845$2585D411-5703-4C7B-865F-3CF7768D7351","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e3a2ef1665994fa1be196a99286cbe26677ab177","datavalue":{"value":"10.1007/978-3-031-40436-8_15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535845$CADB6DCA-56D4-4FB8-A6DD-A280F4AF1E2D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"2dabab20d8dfadef8ff5448ec11941674a12930b","datavalue":{"value":{"entity-type":"item","numeric-id":6535843,"id":"Q6535843"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$E91FD3FD-6F6F-47C5-A4CA-046076074870","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c80bcae4f277c4e50a703e6b182a756f6710909e","datavalue":{"value":{"entity-type":"item","numeric-id":6535844,"id":"Q6535844"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$92174790-B990-4F7A-9E3A-172D116ADA6C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1952080acac824c5abaf90b4ba5029824c97690c","datavalue":{"value":{"time":"+2024-02-28T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6535845$410CE11E-4A95-4987-8411-874C5592791B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535845$6FAA726E-406E-40EF-9D51-C774CE5F1ECB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535845$24F49E51-1AC3-483B-A634-307086043317","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ca2e6254a1d54425672bd8545c24a7853c3c5e95","datavalue":{"value":"7810663","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6535845$4B443308-6AC2-4D39-89DB-8286702C9A64","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d866d2f01ac2c31359811196209e4cb400acaa05","datavalue":{"value":"unifying theories of programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535845$9144FF98-6C26-4BC9-ABDD-363AB733DD02","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535845$0DD2CF27-7A79-4E52-9827-8BC74753D318","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cd182c2e9058301efa292c2afe2941792b9eb1ae","datavalue":{"value":"program algebra","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535845$37B74BE9-8ED2-4015-A221-94996CD9D2E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab20a0363e682206851b94b3be1e96bb56399f58","datavalue":{"value":"refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q6535845$9CA58C9B-94E7-4D24-B7C9-D20931A9F8CF","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":"Q6535845$59752081-0CD2-4F1C-BDA8-CDA1FFBC358F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"77018192936ef221a7216a4ad62b903ce9229b0e","datavalue":{"value":{"entity-type":"item","numeric-id":6045054,"id":"Q6045054"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$043B7ED0-68D9-4FB8-B8CA-B5AB3CAB135B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"02c8f85a04acb0f50025f8744f96b9a09d6922b0","datavalue":{"value":{"entity-type":"item","numeric-id":1982650,"id":"Q1982650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$22F3F31A-DD52-4C2B-A876-EBF4880D9DE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42e8700434177609e5f649d1f5a0b31b34ec0771","datavalue":{"value":{"entity-type":"item","numeric-id":3055747,"id":"Q3055747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$A5096487-AFFF-49EC-A0FB-E0A9EE6080F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f404e88145076a43f26a4aff438db1058e55c891","datavalue":{"value":{"entity-type":"item","numeric-id":2296290,"id":"Q2296290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$796189EA-9FBB-4D9B-B19E-2ACE04340F50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ea00f9571a2f3eb35a08ae82329dd711da0dc8b","datavalue":{"value":{"entity-type":"item","numeric-id":2814613,"id":"Q2814613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$835CB35B-552D-4735-AA6B-AC47A75DD194","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a51285ecc98c7aa36e85f90f6de1b67d1e1af30","datavalue":{"value":{"entity-type":"item","numeric-id":3766810,"id":"Q3766810"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$3C09BFEE-0926-4F6A-95CF-DD3E29935D60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c6b72f9c8f81b8d711ea18b4fe96c1f2fab19a9","datavalue":{"value":{"entity-type":"item","numeric-id":2365393,"id":"Q2365393"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$F91F2822-FA26-4D3C-A30C-42BDEACA5BD9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"deb9865b9ec7d75ea6408f7463449ba93e2c161e","datavalue":{"value":{"entity-type":"item","numeric-id":5307478,"id":"Q5307478"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$3A7CCA09-6CFB-46AE-AEE7-AC53C533017E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3b5e4c8820eb3333a06a963b91456bb31fc1405c","datavalue":{"value":{"entity-type":"item","numeric-id":5219927,"id":"Q5219927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$B10007BC-E0E8-4809-B0A7-5FB814AF14D0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"893a6aaec28db0746fe0bc3a68e85e5a3613dfc9","datavalue":{"value":{"entity-type":"item","numeric-id":4412473,"id":"Q4412473"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$5CB08E97-1967-4BCF-B6D9-7F91952DE9FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f48b4cdf3387b29d116e00769214e58438eb2f1","datavalue":{"value":{"entity-type":"item","numeric-id":2096416,"id":"Q2096416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$BA18B202-531B-4047-BAB9-EF1058F38618","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e428e49b33a6c67633810dab5563be32edf3e18d","datavalue":{"value":{"entity-type":"item","numeric-id":2281663,"id":"Q2281663"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$40BB3C02-AAC8-4002-BE52-5C44D2AA9D04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"70c621d197fc0bb91486b06a843570b23ebff94e","datavalue":{"value":{"entity-type":"item","numeric-id":903516,"id":"Q903516"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6535845$A3E82115-E864-44A3-BD9E-8814FC230057","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5dcfc1459c3178220e1b52f9eed8387bf60d0f86","datavalue":{"value":{"entity-type":"item","numeric-id":2971173,"id":"Q2971173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7bfef54b35c031020c0d7c98cb05d67cb91f96b7","datavalue":{"value":{"amount":"+0.7920892834663391","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":"Q6535845$BB248F5C-C774-4C2A-8A11-95511362B6BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5fe6b82e4f65c76cea46d66440465f4e9c10479e","datavalue":{"value":{"entity-type":"item","numeric-id":6165775,"id":"Q6165775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"16168c083d1202700be55d693291cf120877d179","datavalue":{"value":{"amount":"+0.7312416434288025","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":"Q6535845$21028CC2-8DBA-4163-A4B4-747D24054E76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e185cb3788129a86496b6b33cbf65d270bfb21f","datavalue":{"value":{"entity-type":"item","numeric-id":5327344,"id":"Q5327344"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5eebdbcaf77e9c7de84b3f2c632428cc9bcf59e6","datavalue":{"value":{"amount":"+0.724693775177002","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":"Q6535845$A461726B-6EE4-41CB-8CE4-A1423083B867","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b448852c958cdb0ecc2c93f211b0e5409cc6066e","datavalue":{"value":{"entity-type":"item","numeric-id":5410477,"id":"Q5410477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"774538a142b616ba525f4226cc66e24bd5de97eb","datavalue":{"value":{"amount":"+0.7191590666770935","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":"Q6535845$FDA4196B-1E2C-400B-9ACF-E5AC145605EA","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":"4c6785f00e28b82a54ce3532c1213a92bedc4b7b","datavalue":{"value":{"amount":"+0.7161309123039246","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":"Q6535845$DBA93915-67B7-4E1D-AC36-40A54DF6E9A5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:6535845","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:6535845"}}}}}