{"entities":{"Q3087993":{"pageid":3098708,"ns":120,"title":"Item:Q3087993","lastrevid":51317591,"modified":"2026-01-17T17:56:11Z","type":"item","id":"Q3087993","labels":{"en":{"language":"en","value":"Verifying object-oriented programs with higher-order separation logic in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5940058"}},"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":"Q3087993$1DEEE9F6-D6A5-4CF6-BFD4-CFA0D1DA4B27","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8b2939600588847e63708f7cbb59b23add232d5f","datavalue":{"value":{"text":"Verifying Object-Oriented Programs with Higher-Order Separation Logic in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3087993$1503B083-56F6-400D-897B-87BFA30BB26A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4a23a8fffc92e33abeef873f61b70e2283154240","datavalue":{"value":"1342.68203","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3087993$EC9812DB-AE3E-4F32-963F-5E947C0470EA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"21db8b1984aa88ffc844915d43320885709fd555","datavalue":{"value":"10.1007/978-3-642-22863-6_5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3087993$97278EA7-3046-4C86-A303-87CE39923EBE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4016e1f23463ca2cfa7c5bb34d7ce64f66d3ab32","datavalue":{"value":{"entity-type":"item","numeric-id":287320,"id":"Q287320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$FAD5E224-917B-4935-80E2-1BFD9F031660","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2b996a5e652df381c469ff3488aa7743356a2f83","datavalue":{"value":{"entity-type":"item","numeric-id":2892739,"id":"Q2892739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$70B47424-0FC7-4EBE-A665-639A50860367","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"2d3621dc4f6116fe30692c2581792a932d8de045","datavalue":{"value":{"entity-type":"item","numeric-id":2289096,"id":"Q2289096"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$3D5B4265-DB15-4403-9F39-A62D14FF733E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"573e97e485dc7f23b42802228edbcbd518cf2ea9","datavalue":{"value":{"entity-type":"item","numeric-id":444497,"id":"Q444497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$9A15A6F7-7CE0-4AA3-82A8-2A5A13CDF4A6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$6F25F9FD-D6E2-429C-8179-5E486674F5EC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"cf253edeced6fad2edf52e73f99001914b4fc105","datavalue":{"value":{"time":"+2011-08-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3087993$9BC1C131-51CC-4362-AE8B-BF6DEDBF21D9","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3087993$FB763733-25C4-4332-B7D9-D631D8C45F6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3087993$0CFF8E2A-7A26-4149-B930-9E3A4CC42B7A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3087993$CD373DA0-5774-4A45-86F4-1168FA9FD1ED","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"604b669d1f0c66c3b55a6bd337c8318ecaec0b1f","datavalue":{"value":"5940058","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3087993$04D63A3E-D167-4CFD-97EB-06E4F578E5BE","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":"Q3087993$789E2512-F7D2-40DA-9C69-8193E6105522","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":"Q3087993$12DC372B-95F7-456A-8F0E-A995E6DC81C8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9e318531312e03fb195437e5d9040b42a91afec9","datavalue":{"value":"https://doi.org/10.1007/978-3-642-22863-6_5","type":"string"},"datatype":"url"},"type":"statement","id":"Q3087993$D4A96DED-34FE-410D-889B-B8CD7E0A653B","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"5383b7cf9042193c34f75e1f1431cafdb202342d","datavalue":{"value":"W1848615987","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3087993$E78AC390-0EE2-4DE9-8365-4EAD4558531C","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"84e5cba2f545e4905805f6fbaec8c0259c28fa1a","datavalue":{"value":{"entity-type":"item","numeric-id":4715213,"id":"Q4715213"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$BEADBF7C-8FE1-4EBF-BEB0-4536AD2A6C9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db60aa38e98e0710c59268a6db48219f49912366","datavalue":{"value":{"entity-type":"item","numeric-id":3189790,"id":"Q3189790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$29CBD86E-214F-4E21-B0B3-DA145A815E25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"59ee6ee01b4b1694eb9e94a00a8a009dce26654e","datavalue":{"value":{"entity-type":"item","numeric-id":5316567,"id":"Q5316567"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$114CE086-C278-4664-92C0-D160577F194D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7af4abdec551b3aac3670e5b25a7a3b50d9f3b50","datavalue":{"value":{"entity-type":"item","numeric-id":5408537,"id":"Q5408537"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$8C20D363-4C6E-4A36-A02C-46DA38B29351","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ac394c68c20fbb801a70b3ff9c757f63ef20c2a","datavalue":{"value":{"entity-type":"item","numeric-id":5756495,"id":"Q5756495"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$1C30F15F-104C-4CB4-A66E-8FB04B22ABAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb5c384f83cfe304bd792549ed6786939a461655","datavalue":{"value":{"entity-type":"item","numeric-id":4783297,"id":"Q4783297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$55B7CD52-2914-4A65-BCFD-A6B6863B4D43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1d89278057f829a68cd8215a1e83a3013e2243e","datavalue":{"value":{"entity-type":"item","numeric-id":5276150,"id":"Q5276150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$51AAA8CD-0A96-46D3-BCBA-AA71A08905D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4d35568f9e9d1b4da0eb41e1856ebed95b31b6f8","datavalue":{"value":{"entity-type":"item","numeric-id":3189828,"id":"Q3189828"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$E6C4988C-2283-4C1C-8409-0DC9B5994BD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14d67f54629b43bb24548148f2bbc3f7e8e15eed","datavalue":{"value":{"entity-type":"item","numeric-id":732009,"id":"Q732009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$FD8FD694-6161-4D21-BA88-E88BFB8A3327","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ecd4567de865d75ecbc281a71056a7cdb652c9b9","datavalue":{"value":{"entity-type":"item","numeric-id":3644765,"id":"Q3644765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$78DA0082-65FC-4BB3-92E8-FC6B2C220B74","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13a187f492a2391b57ef98d6cc36cb29fb02ce26","datavalue":{"value":{"entity-type":"item","numeric-id":5415649,"id":"Q5415649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3087993$465B2FBA-D7F7-49D7-89FE-8F7564C39B56","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"150351cfa2021d49b782c50c9d92a501bbc951ea","datavalue":{"value":{"entity-type":"item","numeric-id":2914751,"id":"Q2914751"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"362f6eeb775595661036cda0234c5e04e7f1589e","datavalue":{"value":{"amount":"+0.797575831413269","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":"Q3087993$D6A48F0A-2AC1-4AC3-8195-201326A5CC8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e55d40f9656f79cb943f1db96ffd80edd18eb3b8","datavalue":{"value":{"entity-type":"item","numeric-id":5370856,"id":"Q5370856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9854c143b90cc30568dd3c60ccd890caea21e660","datavalue":{"value":{"amount":"+0.7775031328201294","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":"Q3087993$420BC878-A21D-4DE2-B3AD-A8F1CC2CC3DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d62a3e1ad6d3adcef7c858b6dc71b22aec9d1f7b","datavalue":{"value":{"entity-type":"item","numeric-id":2936804,"id":"Q2936804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7f732196efd66e21469fec3d930566801a3d2f29","datavalue":{"value":{"amount":"+0.7726170420646667","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":"Q3087993$A5815FC2-6F73-422C-8AB7-8388431EB088","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"653bb42b19be8ce2e8f831ce06cf512b9e69994f","datavalue":{"value":{"entity-type":"item","numeric-id":5311261,"id":"Q5311261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f310b18508e966826a19b3cdcc086cc7607532a3","datavalue":{"value":{"amount":"+0.7563068866729736","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":"Q3087993$14CD4D1B-8963-43D2-A2AE-E71F0DAADC31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9ca334c71b2f31093563b1df55327e8a824bfeca","datavalue":{"value":{"entity-type":"item","numeric-id":5415649,"id":"Q5415649"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8fbbca75b166eebfb8d57b4b3de705aa5186c9e3","datavalue":{"value":{"amount":"+0.7524084448814392","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":"Q3087993$03B6EFCB-9AA2-4646-9095-2F321F3D4DFD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3087993","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3087993"}}}}}