{"entities":{"Q5018778":{"pageid":7048355,"ns":120,"title":"Item:Q5018778","lastrevid":54188975,"modified":"2026-01-26T10:37:02Z","type":"item","id":"Q5018778","labels":{"en":{"language":"en","value":"Ready, set, verify! Applying hs-to-coq to real-world Haskell code"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7450477"}},"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":"Q5018778$7B493144-BADE-4FD0-811E-651DB3D07809","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"83be935c8527de18c04005b5afeef8a434c99bf8","datavalue":{"value":{"text":"Ready,<tt>Set</tt>, Verify! Applying<tt>hs-to-coq</tt>to real-world Haskell code","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5018778$660F8DC1-B7F4-48C4-8E5E-C190C4453F19","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ecd908bc00911a9cfd6b4c278b962ecda36b157d","datavalue":{"value":"10.1017/S0956796820000283","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5018778$6A5703F9-783E-454A-8870-5A17ABFC234D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"e4d7002a52efc474bb15cfa83d5abb594bf37213","datavalue":{"value":{"entity-type":"item","numeric-id":375800,"id":"Q375800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$468FE099-5A73-475F-804B-2D496300C7A1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8f46dee8378fa23f4c43e9c15f19fd2b03c0c403","datavalue":{"value":{"entity-type":"item","numeric-id":4689184,"id":"Q4689184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$DDEE920E-A8F2-4EEC-83F0-F498BB3B0392","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a10da9cf5ee82519ae1b329a5d7786376bfab11e","datavalue":{"value":{"entity-type":"item","numeric-id":288195,"id":"Q288195"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$CB28639F-0C4B-4699-A8AF-A51628F8A868","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"686f26ef2102dec34f922caacebd6571ad7fe765","datavalue":{"value":{"entity-type":"item","numeric-id":1786740,"id":"Q1786740"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$29EB5EA4-CC67-4996-ADF2-CC0E36B65EE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1f447da1edce4ea9d6ba9a447a695864117d67c2","datavalue":{"value":{"entity-type":"item","numeric-id":3185840,"id":"Q3185840"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$D8850B63-70A3-4386-854A-1B2781380114","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"e87ce8777d39fe0f74f51a1e962ef974c835f997","datavalue":{"value":{"entity-type":"item","numeric-id":5018777,"id":"Q5018777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$529EC361-FBCF-4302-B556-B5D51BE4CB35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"fe52ffa1b7468cd548841738a45dc4a65b5c47ca","datavalue":{"value":{"entity-type":"item","numeric-id":2763692,"id":"Q2763692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$8D585401-E6E1-4D8C-B152-DF9E97B16A61","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c0cefd96801130048cf3f8ae21032b5cf52d744d","datavalue":{"value":{"entity-type":"item","numeric-id":2713363,"id":"Q2713363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$9F987147-3AB8-4918-B0DC-2052B4E2688B","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ef7e614aee6bc6b48c017c8ec2cbbdd223213048","datavalue":{"value":{"time":"+2021-12-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5018778$9EC2C7A0-8DC5-401D-915F-DD48C38551F8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d9528e24ec4d7900410750b497fa2aaf3eb2e802","datavalue":{"value":"https://arxiv.org/abs/1803.06960","type":"string"},"datatype":"url"},"type":"statement","id":"Q5018778$3F82AC93-BC75-4148-B363-8ABBFB868B12","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5018778$8B2D3BE3-DE4C-45F7-8DE7-C961A6EBDDE3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"6f9cc76eabb62562fc09ec0ab9dd61893d27354d","datavalue":{"value":"7450477","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5018778$DE5D1BDE-E710-42F7-AA75-D38C715713C8","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":"Q5018778$39A90CE4-804F-4E61-85B2-DD59DE4FC84C","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":"Q5018778$DB57BB62-67F8-4ED0-B64A-A4CEED0DF95B","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"20e8225b7fde56abf09e51400675a474f11c4844","datavalue":{"value":{"entity-type":"item","numeric-id":3612435,"id":"Q3612435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$49C4766D-F67E-45B8-B6BD-C73F7AE24269","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1903be4a36187a0a0e197e708bc72f62f93b28bd","datavalue":{"value":{"entity-type":"item","numeric-id":3183520,"id":"Q3183520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$82D7568F-5106-48D4-8108-4ADC92396721","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f8c80f1bc5b87b2a47f6b03fc4a102e9030ce5e","datavalue":{"value":{"entity-type":"item","numeric-id":5747650,"id":"Q5747650"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$5398DF97-DE3F-4621-864E-8F29D90F2411","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"292d5c006305603ea251952b72b3907af5565470","datavalue":{"value":{"entity-type":"item","numeric-id":5176951,"id":"Q5176951"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$7A09C265-C39B-4B86-96D9-D8735753C4F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$2843D00D-2340-4645-A4CF-884718061E30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98589d6fa667da17f782a55cd2dc8c33d4dbf671","datavalue":{"value":{"entity-type":"item","numeric-id":5308710,"id":"Q5308710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$74C37431-9E99-4151-BA1A-3275CF8E1C3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dcf778fe0335efa4c7df1b59a7c13888edd31ba7","datavalue":{"value":{"entity-type":"item","numeric-id":3016214,"id":"Q3016214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$C9C363ED-AADC-406D-91DA-35C7FF051A36","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"935e96858077565d4f78764b795519c8fe29e5cc","datavalue":{"value":{"entity-type":"item","numeric-id":3613436,"id":"Q3613436"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$0019CD53-B3EF-4C64-A678-D0C1B5E83007","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6d1e46bde366c9665559a7c22a84b5c9d3a328b4","datavalue":{"value":{"entity-type":"item","numeric-id":5408415,"id":"Q5408415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$DF5F44B3-A274-4555-86CC-2B453AFED9C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bb1812a83c3a4aee25d6a67b2527c143aea9ae4","datavalue":{"value":{"entity-type":"item","numeric-id":4435471,"id":"Q4435471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$2CBBF483-08FD-4C33-8765-43B3D1BC16FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7d5d08bfafaa2a5e7a91e0a842158a1971c99b9a","datavalue":{"value":{"entity-type":"item","numeric-id":2819693,"id":"Q2819693"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$25C39286-EC06-40DE-B1EF-34879BB8F6C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"227fe77aa9bac83e88e8a7622effb8e94001c51a","datavalue":{"value":{"entity-type":"item","numeric-id":2875232,"id":"Q2875232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$A6E57D5B-B3F5-4E51-AEFA-2AA22E1FE74C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8c5ee97dc07456d2c14cb532ce92e36a757542ca","datavalue":{"value":{"entity-type":"item","numeric-id":4125767,"id":"Q4125767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$921FA1B4-D226-4EB9-808E-4883FCB491DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"561c39284ec9421bb8483b2aeef47c80a5eebeb1","datavalue":{"value":{"entity-type":"item","numeric-id":2829265,"id":"Q2829265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$9E2CA6EF-B78B-4C53-9BA7-79EBF1ADC8AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$89EF8B60-D036-4209-944D-264074D73678","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e6d1f02d1dff7e0706b804b37a3cfa574fb6579","datavalue":{"value":{"entity-type":"item","numeric-id":2982005,"id":"Q2982005"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$B86C75D8-7E73-4D10-95EB-94BDDA186BB9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"49a8d50e2ac3112c2b5beab9a321e48e86e40e67","datavalue":{"value":{"entity-type":"item","numeric-id":4702190,"id":"Q4702190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$619D45D0-17D7-47FB-8629-DE7BD42E2BF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dabf83ea4c060f5e14b4a8648daf2ad197ce4208","datavalue":{"value":{"entity-type":"item","numeric-id":2829268,"id":"Q2829268"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$635E4891-2B8C-4052-A024-69740C02E8E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95ff8e8a966403637a8e7b3a44a0970aabc9f760","datavalue":{"value":{"entity-type":"item","numeric-id":2828265,"id":"Q2828265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$9331CE40-6048-48A2-A397-2B9FE85050AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48b63ef1959c1d3507c45fe9bb1d3548c1c276c9","datavalue":{"value":{"entity-type":"item","numeric-id":5326287,"id":"Q5326287"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$74713E77-B1B7-4CDF-9E0D-C9DB2375BEAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e478b454a848e966dd19d4bc1adbaf619f7c7421","datavalue":{"value":{"entity-type":"item","numeric-id":2819690,"id":"Q2819690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$3F5E4958-782F-4490-911B-73EBB8B6A716","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f02fd528e40655eb782f1320fe4631a9826a756e","datavalue":{"value":{"entity-type":"item","numeric-id":2931819,"id":"Q2931819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5018778$AA863C5D-50A2-4D85-9D3B-B4B5CB5189C1","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b9e7970e95d1351188434a532310522ca80d18b6","datavalue":{"value":{"entity-type":"item","numeric-id":6166140,"id":"Q6166140"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0243d22d404a279f8e0cc2873355ed72b249f25e","datavalue":{"value":{"amount":"+0.7472639083862305","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":"Q5018778$08E757B3-18D5-44E0-BA49-9DC01D3F60C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a637a3ec8530fd323624ddc6f2ba82d813d4aa6","datavalue":{"value":{"entity-type":"item","numeric-id":3546045,"id":"Q3546045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ded44b004f001794bbb106bf2491275ad3740f77","datavalue":{"value":{"amount":"+0.7264845967292786","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":"Q5018778$250C1361-9EEE-4D89-99B7-353E00D5FCC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dad474bf542af9c01dfa65c603f910307ce18a91","datavalue":{"value":{"entity-type":"item","numeric-id":5308710,"id":"Q5308710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"cbbe4d537c884dba855e21e89e1be56e1f212816","datavalue":{"value":{"amount":"+0.723630428314209","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":"Q5018778$C01C205B-03B8-47ED-A70C-0D7E5513FFE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"731b099c7ac38cd7fa2db362ec7da180829ad7e3","datavalue":{"value":{"entity-type":"item","numeric-id":2936807,"id":"Q2936807"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1c4c284db48d68463c02e8ee84add6e9f774d735","datavalue":{"value":{"amount":"+0.7215210795402527","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":"Q5018778$16B1E66F-9B09-4C96-85B3-74C637F9E168","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7f2a3a6dcf7a1e2b6e4a45f6ec641f9802603d1f","datavalue":{"value":{"entity-type":"item","numeric-id":2931819,"id":"Q2931819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7d16d29fd1a6199aae16d1b172de3f9754c941c3","datavalue":{"value":{"amount":"+0.714341402053833","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":"Q5018778$C84C98BE-A370-4E34-A1C0-D201376644AF","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5018778","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5018778"}}}}}