{"entities":{"Q5178765":{"pageid":7208337,"ns":120,"title":"Item:Q5178765","lastrevid":52225775,"modified":"2026-01-21T05:00:15Z","type":"item","id":"Q5178765","labels":{"en":{"language":"en","value":"Ynot: dependent types for imperative programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6415847"}},"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":"Q5178765$2B19BB34-C4D3-46E1-84FA-6047E099755B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2e1d291f36199512db139a0ee3adf44040aa193e","datavalue":{"value":{"text":"Ynot","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5178765$1ECB38C8-D6FA-45C7-999D-A48A344453DB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c453c4da987bac3e8c0d53c9c01eed2c0306c9c0","datavalue":{"value":"1323.68142","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178765$08738BD7-A609-4031-B423-98029661CB04","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"dd14218412ad74702a6950c01524dad86ab38e67","datavalue":{"value":"10.1145/1411204.1411237","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178765$9A7A69F6-91DD-46C8-9FBB-EFD2F240C2E4","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b248d705e0b51ec4722970eaa46ae5f39664514d","datavalue":{"value":{"entity-type":"item","numeric-id":1426867,"id":"Q1426867"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178765$50C86F73-5C50-42B5-8162-33810F0BC7B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1380f7d0e077e40df5a34bb335939f3c6ce8766c","datavalue":{"value":{"entity-type":"item","numeric-id":617975,"id":"Q617975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178765$74157EA2-90AF-4671-9AA6-C8D5ED083F6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"35bf2f3a894a597d19b27b5739e2d0210b5075c4","datavalue":{"value":{"entity-type":"item","numeric-id":2936803,"id":"Q2936803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178765$AD152D02-9E70-4088-B319-B7F305507872","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7dcbe4d24b4e200fdb589ed928c6e44082ee6142","datavalue":{"value":{"entity-type":"item","numeric-id":2936764,"id":"Q2936764"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178765$6B6A68EF-C16F-469E-8F02-CCF640B038E0","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":"Q5178765$C932F7B9-8F26-475D-8B9E-AC0B2162A496","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"6fcd26fe34a7006f4256abb2f15c1ce3abe759df","datavalue":{"value":{"entity-type":"item","numeric-id":5178747,"id":"Q5178747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178765$F3E568E9-370B-43D3-87E4-8158BD15F6CB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"1f27bc284e85649ed8ad3a0b04193a152f9707a9","datavalue":{"value":{"time":"+2015-03-16T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5178765$4E4E8A45-B926-4BFB-BFA6-8DEC80E1AE31","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178765$D8ADD20B-2D58-4C18-AFCF-900DF37B382D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178765$D0BFB1C8-8952-4F3A-BC27-0A18C123D757","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3a45d3b9170142354a54e44062b715a09cdd0db","datavalue":{"value":"68N15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178765$927B4A0E-9141-481D-AC1D-B09990BE2E8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178765$98F4C1B1-B0DB-40A3-B2F3-F32886739110","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5c538da264db4866b87606f9bf0be6dfcb975f16","datavalue":{"value":"6415847","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178765$106D3203-E6EB-4F8B-A127-4DD1A119E92E","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5178765$30D88D99-1162-4432-9B77-6F6A5E904BD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a236a4a9881a761a93f593b6fc0a0e9903a99925","datavalue":{"value":"monads","type":"string"},"datatype":"string"},"type":"statement","id":"Q5178765$340AFC45-735D-4092-BE2A-1CA36716BA08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"938358769b4f58ad078254388a41b1d2ec82e622","datavalue":{"value":"separation logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5178765$CD8DD45D-B665-4298-935E-DF4E4D916342","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q5178765$7514DAF1-80ED-484D-9AF3-2B0A92E749D7","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178765$38EBAB3C-101F-447A-B48D-75729DF4FC63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178765$AF73CA83-5E8C-4521-95DB-65B77C32C213","rank":"normal"},{"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":"Q5178765$C8F1F1A4-1DB5-4872-B4AF-000E44A31469","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"076ade2f424feb4292ee73db98fc22d62f6154a2","datavalue":{"value":{"entity-type":"item","numeric-id":16769,"id":"Q16769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5178765$F40C8BFF-C51C-48BA-860F-AED5747852C6","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":"Q5178765$42FD5A33-94E0-4667-9010-A01AD38F80B9","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"57985ae2caf4e9699784d0140226483cce98f987","datavalue":{"value":"https://doi.org/10.1145/1411204.1411237","type":"string"},"datatype":"url"},"type":"statement","id":"Q5178765$0796CA8E-FB59-41FD-949F-C67BA554EBCC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f1bca3f9574cf7048bdaa5e4b868ffdeaca161e8","datavalue":{"value":"W4245524452","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5178765$AD92F8E8-22D7-4088-8B81-C7AEE5ECD935","rank":"normal"}],"P1643":[{"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":"b9c96856184c142d1b8b3c7edbf9eb3d32371f34","datavalue":{"value":{"amount":"+0.7895451188087463","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":"Q5178765$4C3331DD-646D-4EB9-B5EB-875AF86B2FD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f959c7712c196883e995861185c429abdff17384","datavalue":{"value":{"entity-type":"item","numeric-id":4944851,"id":"Q4944851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7749106a80ce2e00ea6e3ccc396b4d06d4525d7b","datavalue":{"value":{"amount":"+0.7598484754562378","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":"Q5178765$7EFDB955-E60A-464A-80A0-C923EEF5F957","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"91b07f7752f048810838a13b3751f9f4416cde07","datavalue":{"value":{"entity-type":"item","numeric-id":2828265,"id":"Q2828265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ba044645d1d813920a50b59c7a21e0e2a22323cd","datavalue":{"value":{"amount":"+0.750870943069458","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":"Q5178765$8547AFE2-C391-47B6-89CC-2889AF5F1999","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13cececf5dd03a1f6016067f19008279b5c3a46c","datavalue":{"value":{"entity-type":"item","numeric-id":617977,"id":"Q617977"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fd4cc7e9023b0b67ab05e7e1648b48fa0feac0ba","datavalue":{"value":{"amount":"+0.7430471777915955","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":"Q5178765$F4EBA97A-65EC-4FC8-8F2E-C785A198130B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d1bf37c15e48fc38e72aa136040f068ea21e0838","datavalue":{"value":{"entity-type":"item","numeric-id":5417200,"id":"Q5417200"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ccac2403c733e245d834f18766e4036d445dd599","datavalue":{"value":{"amount":"+0.741855800151825","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":"Q5178765$E2EE3948-2B84-4747-A5F1-1365739E2065","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5178765","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5178765"}}}}}