{"entities":{"Q5041105":{"pageid":7070682,"ns":120,"title":"Item:Q5041105","lastrevid":57575901,"modified":"2026-03-31T11:25:37Z","type":"item","id":"Q5041105","labels":{"en":{"language":"en","value":"Connecting higher-order separation logic to a first-order outside world"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7600938"}},"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":"Q5041105$8C7C7E11-8081-4260-AD28-1E5CD18EC6FA","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5764d321f3ce5f9d930f82eb1f372183ef0bfe6c","datavalue":{"value":{"text":"Connecting Higher-Order Separation Logic to a First-Order Outside World","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5041105$FB797DF2-F89C-4DC7-BAEC-E346B9CB08CA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"4908a75805adc8a79daaed43ef96440287e70e9d","datavalue":{"value":"10.1007/978-3-030-44914-8_16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041105$64AB3048-30E6-40D0-82AF-F0CEB9CE1375","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"c6fc9321e1ecf733a02499b42252d991dbda6a54","datavalue":{"value":{"entity-type":"item","numeric-id":1702903,"id":"Q1702903"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$5C25EF90-8A50-4292-90B0-016D5040DBD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7085c2d77a08b4f1954d9d6a78d9d923c48e2271","datavalue":{"value":{"entity-type":"item","numeric-id":5041104,"id":"Q5041104"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$4AFD3A6B-5D8B-4FA3-B4E0-043668148D11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc26ae99955b17096664472ad434caf6f770734f","datavalue":{"value":{"entity-type":"item","numeric-id":1663237,"id":"Q1663237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$36966665-4860-499D-BC47-7D740DEDD236","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7efb66db9d8cc237b51d0f645d1a54c929d4c460","datavalue":{"value":{"entity-type":"item","numeric-id":2789030,"id":"Q2789030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$83F08657-CC03-4844-9C9E-537B6CA2D1E5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f63eb77a6cdb61f75205564f776cc43c0ac4bb43","datavalue":{"value":{"time":"+2022-10-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5041105$F418FD96-F7BF-49AC-86EF-0656B1E10C5D","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041105$FDD1D338-D82C-46AB-9077-FB5D1F703A3B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041105$2E9F461D-D299-456E-A67E-BD67B3B176B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041105$825A10E2-D1D2-4D0E-9545-703B0A1140B5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d68021e614036c105496416b63401a7a5d2f53b6","datavalue":{"value":"7600938","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041105$866F0FCE-CC19-4DD9-AED8-931DF31DC148","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"2eb4d1af95699ef062cce80ecbcf1e1484586450","datavalue":{"value":"formal verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5041105$7136E484-5CAC-401F-9179-59792EF179B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7b98e439d5e7c861a5f9ac5732330ac1976d9d84","datavalue":{"value":"verifying communication","type":"string"},"datatype":"string"},"type":"statement","id":"Q5041105$BA81C62B-476B-4FA2-8289-4F357500E257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"642fb89fab960669bf77c30a5366e85b7fb02243","datavalue":{"value":"modular verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5041105$AF470029-6BAF-4A63-9839-238692022BE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"685e8168d6732ac4339ea8cb44fa865407b14bb7","datavalue":{"value":"interaction trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q5041105$DE3BD2DA-FED3-4FE8-9604-CAA40FFC1ADB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"379cec3fcfbcff38054abae75d5b9f5c6b1c52d0","datavalue":{"value":"VST","type":"string"},"datatype":"string"},"type":"statement","id":"Q5041105$6C8A47C9-2D20-4FF6-BB7D-887F30D0AB55","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"079f0074e9f3a246b8e27b3f58b38d624b7f40c1","datavalue":{"value":"CertiKOS","type":"string"},"datatype":"string"},"type":"statement","id":"Q5041105$49595F23-E0D8-4894-84F0-025D798D0A7B","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7ee2575b4b00dc5c48fe05a1a87740d06a1036d4","datavalue":{"value":{"entity-type":"item","numeric-id":21498,"id":"Q21498"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$934F6E5A-A877-45A9-A2D8-1B21E2E79498","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$BF92E304-BB45-4745-B958-8FDAD1CF2550","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6cc8b602290f72455ceb0d513144a2973b9cf741","datavalue":{"value":{"entity-type":"item","numeric-id":33310,"id":"Q33310"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$BE890813-796F-4A74-9973-C605EBBA85F2","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":"Q5041105$62DDFB1B-D14D-49F1-B9B9-75F2B6B50146","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4e7843cd0c727862f8e2cdef0ebb5d0efc7b15e5","datavalue":{"value":"https://doi.org/10.1007/978-3-030-44914-8_16","type":"string"},"datatype":"url"},"type":"statement","id":"Q5041105$50184BE7-BF16-4ED2-A014-FC42EC92B042","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e7e69d33bee8332fcf1a878190995b45e2c1399e","datavalue":{"value":"W3016373772","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5041105$6EDFE607-135F-44D2-A370-1B919DD01557","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c46319975d5f428b28cf95457785c347fec2d0df","datavalue":{"value":{"entity-type":"item","numeric-id":5494381,"id":"Q5494381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$05B2D9C9-43F1-4638-A654-1AC56BE05978","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"127db5097e77e5b4edc8afc4e762efcd27117ed4","datavalue":{"value":{"entity-type":"item","numeric-id":2931804,"id":"Q2931804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$FDCA5EB1-0815-4095-896A-33512225487C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"73901d66c4278581e8cce3d77cced49f915057d4","datavalue":{"value":{"entity-type":"item","numeric-id":2819848,"id":"Q2819848"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$51072CB1-ACF8-4595-9694-E7CC828169F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"567a8dff2d0b10b014f06f4bbf8ecdbec1e09916","datavalue":{"value":{"entity-type":"item","numeric-id":2988660,"id":"Q2988660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$AAF6A204-2C11-42EB-AF94-A32A658E695B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f9e4d418853bd2f740df9013cb7e6d403808721","datavalue":{"value":{"entity-type":"item","numeric-id":2985775,"id":"Q2985775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$4D6ACAB3-C015-484C-A90C-0E199E9099B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2934261f50a1e0b490a2bf100b0d26006aa930a","datavalue":{"value":{"entity-type":"item","numeric-id":2931839,"id":"Q2931839"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$D7F1A3E0-16EE-4052-86B2-64A72E03FD52","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ec596191c58c0192912d43559518df53cc026d8f","datavalue":{"value":{"entity-type":"item","numeric-id":879368,"id":"Q879368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$7FAF606E-3995-4C3D-9699-BDB66A260659","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03f3f16581119d55405062987de2f3afde2cc2f0","datavalue":{"value":{"entity-type":"item","numeric-id":2802435,"id":"Q2802435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$60FBFB94-EF40-4CC3-B812-88F22155BA44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cbae59cabb692e5aadee25ba2669315a1892bf3e","datavalue":{"value":{"entity-type":"item","numeric-id":2802440,"id":"Q2802440"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$E6722695-9C82-4A7C-B947-17AF4921C284","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"302effae99d5b630a1a547d06432f2bd4b8bfd35","datavalue":{"value":{"entity-type":"item","numeric-id":3613364,"id":"Q3613364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e5209dbcd30230f11f97634bcf2308641622e26f","datavalue":{"value":{"amount":"+0.7455018162727356","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":"Q5041105$E590FEFB-CDA0-4282-85D4-4CE4FB9E892D","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":"f2b5c51f5305ea8880e88e589633153dadee6af6","datavalue":{"value":{"amount":"+0.7431202530860901","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":"Q5041105$B80A360E-E26A-4B44-8EED-C554E31FE9A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"54945991e72c4e075bbdaee9b84ef77985d61019","datavalue":{"value":{"entity-type":"item","numeric-id":3087993,"id":"Q3087993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7857cb6f292574945111b7355890cf3660ee8cbb","datavalue":{"value":{"amount":"+0.7331212759017944","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":"Q5041105$00E24B6B-DA9B-4F00-BD7E-6752EFE55130","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c5594c5bf46853afd45fe569c6973438c14d73eb","datavalue":{"value":{"entity-type":"item","numeric-id":5494381,"id":"Q5494381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cd4d5c003e96612dffc921c7a34eb8f4fc11fadd","datavalue":{"value":{"amount":"+0.731510579586029","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":"Q5041105$1B7C70E5-944B-47D6-91CA-6A52BBFAB09F","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":"dcb4ae35075d623ea1db445b7be7a1f95f64689b","datavalue":{"value":{"amount":"+0.7286651730537415","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":"Q5041105$CDD5290F-1CE5-47AA-8FA6-68A6240BDEA4","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5041105$E0E4ECBA-C929-4FC2-BED1-D5420DB32C85","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5041105","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5041105"}}}}}