{"entities":{"Q1744423":{"pageid":1755165,"ns":120,"title":"Item:Q1744423","lastrevid":72418443,"modified":"2026-04-14T04:46:28Z","type":"item","id":"Q1744423","labels":{"en":{"language":"en","value":"Proving correctness of a compiler using step-indexed logical relations"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6862950"}},"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":"Q1744423$4CC06544-5C3B-4B72-BB6F-D91CB03933B8","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7dd931aed152bc294b67b00f927531ae04b7e86f","datavalue":{"value":{"text":"Proving correctness of a compiler using step-indexed logical relations","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1744423$DCB4AD21-20CA-4A5B-93DA-ECBF89DAE577","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7b7d4a7537e0437dd1408ace656eadd41a82db11","datavalue":{"value":"1401.68035","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1744423$00E67602-8B9B-4D36-B1B2-55C80107FF30","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"45d85afdee5f39d36a7124eed2054401b5d977e3","datavalue":{"value":{"entity-type":"item","numeric-id":1744420,"id":"Q1744420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$CE80D591-F03A-46FF-821F-C633E61433E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"09573ab70c9d986235750625015542077d5f5980","datavalue":{"value":{"entity-type":"item","numeric-id":1744421,"id":"Q1744421"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$AFA2CC09-3BF6-47B2-97C4-BDBD29D755A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"55e641319c011b54f0c69b6edb09640a3dbb847a","datavalue":{"value":{"entity-type":"item","numeric-id":1744422,"id":"Q1744422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$0429D8D1-EC3B-485B-B8B1-1FEAD6BF52C0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8b5474500ed23a367f35223f2b97230670493d7c","datavalue":{"value":{"time":"+2018-04-23T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1744423$CBB6A703-EBA8-4253-AE10-E663E5DD8CFA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3affb2aa66be15f2a63c60d2aaa92bd143e6d46","datavalue":{"value":"68N20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1744423$26A96F12-D742-440B-BC4E-4BFB5A7BA2FB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1744423$9BAC415D-E049-45C0-9721-77A2F99370DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1744423$646267E7-C066-4E52-8AA2-5AB223ACDAF5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b8d6136445e16dd85543b3bd1e46c3e8d40f97c1","datavalue":{"value":"6862950","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1744423$842E3D96-1CDF-4E1D-86F8-DAB65F4C2718","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"acd9c52c59d07d5822d39f1d47e4205b4637b9d3","datavalue":{"value":"compiler verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q1744423$BDBC0C15-65AA-4F1C-9D84-2F24868A2981","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q1744423$E4935F6E-A403-41AB-A992-66EEEC7D111E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cc5688260d56258e4916c5f7e7a5117477dbc3ee","datavalue":{"value":"biorthogonality","type":"string"},"datatype":"string"},"type":"statement","id":"Q1744423$B51BE313-6E46-4836-93E1-B45399400134","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"905b948fe4bfdb7eb3dea0f42ea8b556d62e1229","datavalue":{"value":"step-indexed logical relations","type":"string"},"datatype":"string"},"type":"statement","id":"Q1744423$6EB0802D-5F91-41E5-AFF8-D18FF8CB0354","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"d5c77afdc1ac83608a284df9842841f4522194fa","datavalue":{"value":"Q113317678","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1744423$20D83382-801C-455B-AAEA-47BBD99D03FD","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":"Q1744423$9F56FB40-5456-47E0-82D1-DA8E6B1AB5F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"328a4887d5a745918f682c9b5cd832468b1041c7","datavalue":{"value":{"entity-type":"item","numeric-id":21718,"id":"Q21718"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$2C26ED9C-ACAF-40F3-ACCE-F70AF13BEB49","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":"Q1744423$B74F65EB-613B-4EFF-BA93-35CDC55F1F8D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b78a04e8a584c16f1e3b93816e024078fe5ea5cd","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2016.06.013","type":"string"},"datatype":"url"},"type":"statement","id":"Q1744423$72A024A2-C525-4FC7-8F80-7FB5B99B1D3F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"48b412f1ffc430f9b25ed85cab93d76934b7be50","datavalue":{"value":"W2474272294","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1744423$AD0694D3-5227-4F13-ACDC-2C82CC3958A3","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3e540e9037d6b40bc6045b99bb685bc55f586971","datavalue":{"value":{"entity-type":"item","numeric-id":5899009,"id":"Q5899009"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$AF0959C0-5181-47E1-B792-C54F34C963A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ed5124fab1d64feb8b4feb25646b660a09eb4cd","datavalue":{"value":{"entity-type":"item","numeric-id":3523161,"id":"Q3523161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$7E3462C1-97C4-4EBC-B6E6-D16860663537","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"05417919433e4d5ed4f85fc6474f5b255b9fe668","datavalue":{"value":{"entity-type":"item","numeric-id":2936808,"id":"Q2936808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$083E924A-956C-41EA-83D7-FB4B947E7D3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d16ee5e65f1db51f9c436dbb90be9daf0b8247a","datavalue":{"value":{"entity-type":"item","numeric-id":5255065,"id":"Q5255065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$0FA3E50B-F73C-4509-9095-C62336257755","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"145e622600d34e2e2f04dd6d81034ed240f20627","datavalue":{"value":{"entity-type":"item","numeric-id":5176935,"id":"Q5176935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$C5C524A2-6357-426F-B1F3-42F3B71F0012","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c3ace06db1892d761ccecefca66e1592cc981c11","datavalue":{"value":{"entity-type":"item","numeric-id":3625516,"id":"Q3625516"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$E5F06DDE-5594-4F64-A135-6D9B20EEF499","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c1e93b7524b60bb9ab3f8d71fd24ac2451f79309","datavalue":{"value":{"entity-type":"item","numeric-id":1326769,"id":"Q1326769"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$318401A5-9A71-4C41-82F4-B75CBF7846DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"442937e7a92071855338b0012339d681574f358b","datavalue":{"value":{"entity-type":"item","numeric-id":2464723,"id":"Q2464723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$4CC1586B-2FA8-4CD3-8DA1-0CDA5566F503","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"87f7bcfffc49742b219cd84a695191ca8beef7cd","datavalue":{"value":{"entity-type":"item","numeric-id":5734774,"id":"Q5734774"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$18564B31-1D2F-4328-A999-E931EDA7DCDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43463c3e0ec0180b5df962e03623cf8b1930330f","datavalue":{"value":{"entity-type":"item","numeric-id":3060983,"id":"Q3060983"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$4DEDD06B-2DAE-45FA-A316-2F9D4B1DDF13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fca3c893ec274449af409e1d364b4d648dd50b27","datavalue":{"value":{"entity-type":"item","numeric-id":1012129,"id":"Q1012129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$2E149103-DA1F-4ED7-A93F-EFC9594332F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1428c9a5a31636248fc81852945e32ffa3323d8","datavalue":{"value":{"entity-type":"item","numeric-id":5574395,"id":"Q5574395"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$D6621626-7733-45B5-8AEF-31101839E0B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e4ac9603abd6f7de6f4a20233ef4e949886e94f","datavalue":{"value":{"entity-type":"item","numeric-id":4068067,"id":"Q4068067"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$57890EAF-9DE1-4CF2-B3DA-04750BA00375","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9e58509c58589e7e9ff957b836ae2fde24359d4","datavalue":{"value":{"entity-type":"item","numeric-id":5834612,"id":"Q5834612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$15122810-6D4A-4DDE-BAEB-4E143F720CB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f2421034b2e5b8c9a4605f25882b5ef4d7bb9c2","datavalue":{"value":{"entity-type":"item","numeric-id":2704328,"id":"Q2704328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$4D839DC6-658F-4930-B11E-FA826D23F16E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2edfda0e229947f3a16f4624eaf252fe910fff41","datavalue":{"value":{"entity-type":"item","numeric-id":5096244,"id":"Q5096244"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$6514FE5D-7121-45C8-A0E9-6F7F4B0738DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"31252629cba48d38d03cb7b678ba549427c4e4f5","datavalue":{"value":{"entity-type":"item","numeric-id":2968419,"id":"Q2968419"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$7E6A97F0-789B-47E5-9610-02338D8F81E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d80b1ce6c7c55e134225781cab112803b76b1488","datavalue":{"value":{"entity-type":"item","numeric-id":4358457,"id":"Q4358457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1744423$3203475C-CF4C-4437-BED3-D16182C5D6C8","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f247b590f7c7cbc30326d01d82bc76476a14e38b","datavalue":{"value":"10.1016/J.ENTCS.2016.06.013","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1744423$137B07F0-CE09-4358-ACA3-16902C8FDB7E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"258ed35583a03b29ffa76d971860ac7fd556d874","datavalue":{"value":{"entity-type":"item","numeric-id":2936808,"id":"Q2936808"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f3b3b0e8343bf3487d9a7a3d415a15630455b998","datavalue":{"value":{"amount":"+0.8598589301109314","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":"Q1744423$794FF934-C682-49B2-85A8-5733ABEBC18A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f29474da1eb824221d8a9a3b9e4e3876194dc88","datavalue":{"value":{"entity-type":"item","numeric-id":5348912,"id":"Q5348912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35b7365e354aaa7955476e290becd9b12f7de169","datavalue":{"value":{"amount":"+0.7593645453453064","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":"Q1744423$AE7798F0-D1BE-4B3F-9F73-E8D8FCED47C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"753995a7591fdc07125446e04545c9e631973be2","datavalue":{"value":{"entity-type":"item","numeric-id":4474853,"id":"Q4474853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96394a5c9af0ba74aa478bb70bc34c17b1c31bbc","datavalue":{"value":{"amount":"+0.7545368075370789","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":"Q1744423$C546BA87-A8DB-435F-89BB-9E9530290A71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a79e76fe41baa7869d6e8c24476d7f501810bf34","datavalue":{"value":{"entity-type":"item","numeric-id":5408538,"id":"Q5408538"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"5d4d49ff822388da19472251f77900cefcd99ddb","datavalue":{"value":{"amount":"+0.7519017457962036","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":"Q1744423$37A6A042-0866-4B4C-AD84-E0A0001BE2EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2850ffe00faef318a0f700478b55c4e9c6197b5a","datavalue":{"value":{"entity-type":"item","numeric-id":3677148,"id":"Q3677148"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9f0685e6ae5e90460e26e6aa1c576013ff1a416","datavalue":{"value":{"amount":"+0.7491021156311035","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":"Q1744423$5A611BCE-C9BA-4633-BD07-ADB779D9A5A9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Proving correctness of a compiler using step-indexed logical relations","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Proving_correctness_of_a_compiler_using_step-indexed_logical_relations"}}}}}