{"entities":{"Q5370856":{"pageid":7400430,"ns":120,"title":"Item:Q5370856","lastrevid":40994279,"modified":"2025-04-17T02:28:38Z","type":"item","id":"Q5370856","labels":{"en":{"language":"en","value":"Interactive proofs in higher-order concurrent separation logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6794653"}},"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":"Q5370856$D2FAF909-77C0-4EAD-8E16-DB3E571BFC84","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"bd735f20160f6ba337a4aed1d9cabbafa6540913","datavalue":{"value":{"text":"Interactive proofs in higher-order concurrent separation logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5370856$6B49BD80-3257-41A4-B91C-6D6C2C15793A","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"870ca621b2371cd74cd2d98220e5525a61bbf49c","datavalue":{"value":"1380.68341","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370856$2E4038C7-E072-4D6E-9F3B-AC9384A13071","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"a17e3aaf3ac80e68fde64a610ac687c491f6f67c","datavalue":{"value":"10.1145/3009837.3009855","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370856$B281CE02-F97C-44EB-8C62-C42B6926352E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d784fe6cc5179886bfe36c86ddc8bdd92ade5a26","datavalue":{"value":{"entity-type":"item","numeric-id":549190,"id":"Q549190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370856$FC006CEE-3DD9-4DFE-95E0-3157DB5C2B76","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"52254dabb8af5997f12cdfe0722d50f0619c8ae0","datavalue":{"value":{"entity-type":"item","numeric-id":2787452,"id":"Q2787452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370856$B74AA897-4067-4F56-BCDE-EEA255D9D73B","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":"Q5370856$C127993B-1B21-49C3-A6B8-64D668046005","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"e2300a4bb532724f6695014ad32dc9335c9fdde3","datavalue":{"value":{"entity-type":"item","numeric-id":5370840,"id":"Q5370840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5370856$3415F291-F207-430E-9859-131885B12FBD","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"6c23b22abb6cd47509eac4c3e5d58b13717e9ea4","datavalue":{"value":{"time":"+2017-10-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":"Q5370856$671BBC0E-C133-4C79-94AF-FC0E63358077","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"cd2cd4b308475237e6883da2a5187f0917890aa6","datavalue":{"value":"https://lirias.kuleuven.be/handle/123456789/553559","type":"string"},"datatype":"url"},"type":"statement","id":"Q5370856$8BBF6B9A-5ADE-49FB-A10B-86F9D40A7C9F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370856$B761719F-32EB-477A-9F40-EA82D554B50E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370856$140862E5-C31A-437C-966A-AA40A1597A75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370856$AB421EF3-7819-46B5-9623-53B6918660C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370856$12264DF3-D880-443C-B461-C628D452360D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8f412c62952107f7ff74e77578c2ab25d3e121a","datavalue":{"value":"68Q85","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370856$7F991D32-3934-49B3-B6C0-6A4D672FECF2","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"f42f6995771c557e0bd698967183ecd8382df1e9","datavalue":{"value":"6794653","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370856$7EB1651B-CB2D-4FBD-A757-19BAF1A4E09B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370856$33D06EC4-4488-4708-8D94-53CAA29C7B80","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"59c0ff791bef59c18e0be5c681d736f264593fa9","datavalue":{"value":"fine-grained concurrency","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370856$7956CDC1-F405-444E-A651-4EF0D6E7943F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"21cf102e52d55bb9e3ba4ca1c32b8839281988dc","datavalue":{"value":"interactive theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370856$C3268510-EBF9-44E1-A4D5-2993C825D1BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"02e2bd1176be2ca24a8b368e42bc8812510b3ef7","datavalue":{"value":"logical relations","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370856$6A8CE4B7-8C07-4791-9128-9CCF692FFF10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5370856$EA553A2F-CFFE-4D49-A426-F4CC4CE10CFF","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":"Q5370856$2E992266-68D4-43CA-A0B7-D00BD0C6B616","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":"Q5370856$91FBE083-6609-415F-A21B-B9FDE2D6BA20","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0e45c68b8363eda3a03527d6d9127d65b38b7dad","datavalue":{"value":"W2562833768","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370856$4FF78C63-E227-4A9B-9E58-8F782AEA5FB6","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"bcf2f3edeb3d8a4941cc848a4146ebc9a2b2b89b","datavalue":{"value":"Q130853219","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5370856$4C31A554-EBC6-490E-8054-A4601153FDDC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"209e48917fd84091488eb19cfdff912f10b1e410","datavalue":{"value":{"entity-type":"item","numeric-id":5872872,"id":"Q5872872"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3d3d6ac64b34bd042fde854ad588281a654b61bf","datavalue":{"value":{"amount":"+0.9288639","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5370856$0D5AAD2E-BC1E-443C-B76D-6AABDC223944","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef476b6e9f92d21b9e2dd87111ddd904f4837c06","datavalue":{"value":{"entity-type":"item","numeric-id":2151405,"id":"Q2151405"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"553b4bd0272f1ba95dfda512b25f93be68fbdee3","datavalue":{"value":{"amount":"+0.92886376","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5370856$12410468-A3F9-424E-875D-B6B44D3F3873","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f9753d67bb44c3e85764be086f9ac5baf42f744","datavalue":{"value":{"entity-type":"item","numeric-id":2936240,"id":"Q2936240"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f8039d007a680213a1c9acb94b25bbb960be022d","datavalue":{"value":{"amount":"+0.9110419","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5370856$8335F4AC-6697-46A4-B68C-E0FE1DDC33DB","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":"fdfc49465fcca9ef49200f5abe215647220bbc5a","datavalue":{"value":{"amount":"+0.9110394","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5370856$CDC85C02-E8E8-42F4-A251-D0C0AA3AA25B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5be0a1b701db6fca2da35be5fdb6e7b38d0bcdb1","datavalue":{"value":{"entity-type":"item","numeric-id":2988664,"id":"Q2988664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"43c76c29ded8c3d2f104b289546c9dd4214ed871","datavalue":{"value":{"amount":"+0.9041183","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5370856$A1D34B8A-4352-4F21-8365-6F7B2D420D0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"df98aae22bb1683b064165c2fa3cf3b0d4f27c56","datavalue":{"value":{"entity-type":"item","numeric-id":5428268,"id":"Q5428268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"db07741e8eac94efcebd24a3392f2271c58988b5","datavalue":{"value":{"amount":"+0.8941229","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5370856$29ACB08A-12D6-4A68-877A-541656AEC613","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9544de41f81387be86297869277c1a82bc01c1b7","datavalue":{"value":{"entity-type":"item","numeric-id":879367,"id":"Q879367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4121c68273a8050eaa6f7070e95ad07c4a0e8ef3","datavalue":{"value":{"amount":"+0.89124936","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5370856$2DCF1D28-41D3-4D15-84D8-D87D89F76F92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"96f72112ae0de9c4ec7fdaff364082f56a8eeb23","datavalue":{"value":{"entity-type":"item","numeric-id":5311481,"id":"Q5311481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4121c68273a8050eaa6f7070e95ad07c4a0e8ef3","datavalue":{"value":{"amount":"+0.89124936","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5370856$343776DA-860E-4BBD-9DCC-898E7696FBD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb07a55d65e4f95d6f280adf9b89a0c21536434d","datavalue":{"value":{"entity-type":"item","numeric-id":4535028,"id":"Q4535028"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fe7b9566b53a1d531dc3167200e289e265e53e17","datavalue":{"value":{"amount":"+0.89040524","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q5370856$D961338F-C0F3-4E24-8DE0-86FCD3CCB33A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5370856","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5370856"}}}}}