{"entities":{"Q5505511":{"pageid":7535071,"ns":120,"title":"Item:Q5505511","lastrevid":96531335,"modified":"2026-06-05T11:31:38Z","type":"item","id":"Q5505511","labels":{"en":{"language":"en","value":"Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5498235"}},"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":"Q5505511$CEC10C79-7527-45D7-A3D0-EB42C4B7C364","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"44cb02ac6d332af17affcb5154f4709b897724a0","datavalue":{"value":{"text":"Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5505511$B7E43A60-953A-49A3-8C79-521CF1308741","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"efb32f16a42cbfe329a07642a59e12b30a1ceeb4","datavalue":{"value":"1166.68348","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505511$C1061288-E42A-473D-863C-A98BE424A5AE","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ee1f343e522c22dc0967a3d5e1fb8c80fddd1950","datavalue":{"value":"10.1007/978-3-540-85110-3_25","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505511$9F964F7F-CEFC-410E-B7FB-CCF99BF664C3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f71b6b0d8fbb0cb846e7832cd3e9260cda3a8981","datavalue":{"value":{"entity-type":"item","numeric-id":1012149,"id":"Q1012149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505511$C666A275-089E-4988-AC0B-392E6D706B9B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"5939133e36fb4feff360b4227a7d2c3c1f7afed9","datavalue":{"value":{"entity-type":"item","numeric-id":1012150,"id":"Q1012150"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505511$91CB2423-19CE-47F4-8DBD-74FDCE77897A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b006a6cb5e94794d8a0a2db987b90a98cbabb8cc","datavalue":{"value":{"entity-type":"item","numeric-id":5505510,"id":"Q5505510"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505511$DD0D0E10-9A15-49BC-82F5-5176CF9ED396","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5505511$00BBB6CE-E76C-4209-ADE6-BD94C5B1BFB4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"51e6c39ac6ec91b8381a06fe1e16cf5aca0f2bdc","datavalue":{"value":{"time":"+2009-01-27T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5505511$6D6A7B9E-078F-4159-A740-10C81649E95B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505511$2A73A859-6040-4AB1-8786-963DFCC8B519","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505511$E2CE3437-0573-4632-9C13-2DE098B104A7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505511$F1246AEA-4B3A-47BD-BE3B-3DC649EAB1E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a50ad10d859c37581a66df0bd2c759d3d47ad6a4","datavalue":{"value":"68U35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505511$014F4AA0-3337-436A-AE01-007EDC7B34CC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7d59cd61aef23be84fa6505a92d3bb6f4c98a8bd","datavalue":{"value":"5498235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505511$F2703B1C-FC20-4849-A74F-570B5113DC70","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f02f4db7bd17ba3fbae1be6bcee13dc9e5aa86bc","datavalue":{"value":"formal methods","type":"string"},"datatype":"string"},"type":"statement","id":"Q5505511$339D6A55-F10D-4D5B-807E-EA8BDCC6C26C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6ff93fcab863d9a2d7b61f398ca8507531735efa","datavalue":{"value":"software verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5505511$8EB147A8-D3D5-4F56-B587-3254E9D4496C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b36661f0a3390102be2be05796702400601b738","datavalue":{"value":"theorem provers","type":"string"},"datatype":"string"},"type":"statement","id":"Q5505511$B0AB922F-996D-44BD-A7D7-2057F1E33C63","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"00b76a2e54f8798fe172effecd557ced03e2f904","datavalue":{"value":"functional programming","type":"string"},"datatype":"string"},"type":"statement","id":"Q5505511$1E62C2F0-075A-4363-A9DD-6269458E59EF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"234248f3195c943b3c21c62521d93b31f473edc9","datavalue":{"value":"real-world applications","type":"string"},"datatype":"string"},"type":"statement","id":"Q5505511$87A5D720-3547-4FD5-B232-A6D830152A07","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":"Q5505511$102CE7C5-478C-42CE-910B-2D8D78721BE8","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":"Q5505511$A8CB0B01-653D-4B0F-8664-10716D12C83A","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7fcadbe23ca7bb414532a373c4d6c4444b0c2a1f","datavalue":{"value":"https://doi.org/10.1007/978-3-540-85110-3_25","type":"string"},"datatype":"url"},"type":"statement","id":"Q5505511$C617EF6B-6DCE-4825-AAF5-7D3C1818D0D7","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9e99e310082d9a6823226740c6289d939f7aac6d","datavalue":{"value":"W1555957476","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5505511$8C21B66E-68A6-4367-A5F1-57AD4ED8F38C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5fd0a3da52619271d7c219229b2e58d75d6b92b6","datavalue":{"value":{"entity-type":"item","numeric-id":4418578,"id":"Q4418578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"95360a5a961b73e9d4b11ec0e3bb36b6df5e5869","datavalue":{"value":{"amount":"+0.7116455435752869","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":"Q5505511$9A964384-9340-452C-AA48-8FD01A77DA14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"009ffe0b8825f9515ffa02187a661a990f5a0c02","datavalue":{"value":{"entity-type":"item","numeric-id":4037395,"id":"Q4037395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c5c50c8453da603e68c08dc99a86c7f5a64c18c1","datavalue":{"value":{"amount":"+0.7054772973060608","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":"Q5505511$23D9E073-643D-46F1-87CB-C944B9C90979","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d5d3a9bfaa35aeb9a6c1d64c9f4dc2c86ed3ca4","datavalue":{"value":{"entity-type":"item","numeric-id":4357063,"id":"Q4357063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fdadbccf44a1555d08b5e880895655c3c8433e93","datavalue":{"value":{"amount":"+0.7053412199020386","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":"Q5505511$3C8EC4F2-06C9-441D-B1DA-A6800B7A014B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69176cbbc54dd7ef46e8eb8e2624dbcf54a8297b","datavalue":{"value":{"entity-type":"item","numeric-id":4037098,"id":"Q4037098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ce3cb63fc8b5076ec9d04b1bbccdd2649fd0b965","datavalue":{"value":{"amount":"+0.7005714774131775","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":"Q5505511$79255A54-969C-415A-AECE-D54E0D966F3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3320d2109578c47d0aaaa2f9f9a21e0e10eb9554","datavalue":{"value":{"entity-type":"item","numeric-id":1702892,"id":"Q1702892"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1d837a4b2de2a7a20e53e7c7de4c236d405db314","datavalue":{"value":{"amount":"+0.6966204643249512","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":"Q5505511$2D3D9E27-8652-4DEE-9793-9DC6E5CED052","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Using_Coq_to_Prove_Properties_of_the_Cache_Level_of_a_Functional_Video-on-Demand_Server"}}}}}