{"entities":{"Q4645809":{"pageid":6675390,"ns":120,"title":"Item:Q4645809","lastrevid":41180546,"modified":"2025-04-18T19:02:45Z","type":"item","id":"Q4645809","labels":{"en":{"language":"en","value":"The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7000087"}},"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":"Q4645809$854C138C-5001-4180-A79F-AB30AC464548","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"5d392003390bf2d15322123bd9d688cff2e7445e","datavalue":{"value":{"text":"The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4645809$990FE5FC-7592-4C03-B1A1-60E5D78D2FC0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a0b820831f06443af303b744eae1c3aa3671f7ef","datavalue":{"value":"1407.68091","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645809$B7F4634F-C39A-4925-AE88-B9391528B4F1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ec5d8cd0e8123f492ff6f56352e4ef071770c2cd","datavalue":{"value":"10.1007/3-540-61254-8_24","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645809$B50CF391-978E-4F41-BD6A-59053349A36B","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"89f7a0f36664aed5fbf40f464b0ffed3f5d83ba2","datavalue":{"value":{"entity-type":"item","numeric-id":4474852,"id":"Q4474852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$029B8C78-1A80-4DE0-8781-ED5AA87E2985","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7191134f319418d58727fd4a71fc323f51bc3b02","datavalue":{"value":{"entity-type":"item","numeric-id":714619,"id":"Q714619"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$07A20A2E-9DFF-4BE2-9130-A7E38C0CCF6D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f4e0f8e524361885297eed7490a40202225a697e","datavalue":{"value":{"entity-type":"item","numeric-id":4645800,"id":"Q4645800"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$72298656-CF75-49DE-81D1-2D07AEF96062","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9c0a1786c627d23fd7437b6a14326c56be749770","datavalue":{"value":{"time":"+2019-01-11T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4645809$AAE9EDBD-56CD-4850-B361-BD796B1253E8","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645809$D8B6B3B3-4230-41F7-A2DB-A9358D788375","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c636094cc8b933189eabd7c009d327f829bc6ac4","datavalue":{"value":"68Q42","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645809$B801A16C-8BEA-44BC-AAE0-2ED7CAB970DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645809$605191E3-5D64-46AB-9307-FD35CE7723DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645809$E5E85975-B7DA-4827-BD08-1C446A0D30F5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"130c983be27a34053569c7096425fcb47ce914e1","datavalue":{"value":"7000087","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645809$8FD1ADA4-4423-483F-977B-A73D2CBFD6C2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8bf549142b710f01581b24fd28cbb67614316cd4","datavalue":{"value":"theorem prover","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645809$C98B79B1-5A20-4517-BF62-CF1875A6BEAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d15a5b88457b15e43f49d0900c124a1c1adc72df","datavalue":{"value":"operational semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645809$88E8408A-5FA5-4408-8E12-6E28083E4231","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"854c00e8d24a55ad2ac54a90d02cefdf16b5ce4d","datavalue":{"value":"abstract machine","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645809$CBAC22E6-C611-4948-94B5-6B00F08F413F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ea290032d710a04356408d10e3e939703353014e","datavalue":{"value":"functional language","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645809$D31EB705-01C2-44F9-A7A3-52D749CD768E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"51802126f63d5102d578f2858428d5d0f09da73b","datavalue":{"value":"denotational semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q4645809$998CA755-415E-4C23-91D0-94B1E69FAD54","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$798E180E-21E7-4F13-908E-03AC43A80F35","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":"Q4645809$48931DB4-54E8-4B9A-80A7-64482B4794B5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"106b45b74d03fe8f6bf1b7770a648929f3b3eb1b","datavalue":{"value":"https://doi.org/10.1007/3-540-61254-8_24","type":"string"},"datatype":"url"},"type":"statement","id":"Q4645809$D7A61045-6133-43FA-A227-A88F15B9CDF5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3dce2f7f509f09b1df3bf2648c6dc99895e8b505","datavalue":{"value":"W1492125303","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4645809$88C1F1F5-1BA7-415A-A4A8-32BB84879006","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"86ff5d819d7b87fc96425d66dc0c9a0ecab05cd3","datavalue":{"value":{"entity-type":"item","numeric-id":4222771,"id":"Q4222771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$B9B3A76C-A3CD-4278-B65D-B9970D3EECA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cff4a89cd80c0c7e8c521abbd889f8b98ac1a3eb","datavalue":{"value":{"entity-type":"item","numeric-id":4311530,"id":"Q4311530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$1B67098C-9D86-4D25-AA40-78BFCB13E35B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c8eba0cc54e413651d250aafae961a0f9641814","datavalue":{"value":{"entity-type":"item","numeric-id":4474853,"id":"Q4474853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$C81840AF-2BF2-4C02-94B8-C8511B9AE874","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14821703ad3559ce115eabb18820913df4a58412","datavalue":{"value":{"entity-type":"item","numeric-id":3202991,"id":"Q3202991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$EBF9BAC1-ADA1-48C0-85AF-443827013928","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3a1fd100ba49d79341053b43b60105b7dfb1c67","datavalue":{"value":{"entity-type":"item","numeric-id":4023587,"id":"Q4023587"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$FB675996-FB8A-4B3D-8251-0DA3CF507537","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a10bbeb6c6903ace983b2dbf286a2ef4e5b248ab","datavalue":{"value":{"entity-type":"item","numeric-id":1331625,"id":"Q1331625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$99DD8AC8-BE2B-44E9-BBC5-841AEDDDD20B","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":"Q4645809$1A35A072-B348-40F8-9C8F-6A1252BE2D06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"21696c6ff1814194355f64378a4ee4b398c3f782","datavalue":{"value":{"entity-type":"item","numeric-id":5890041,"id":"Q5890041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$6145D990-A747-46C0-97FB-DE586A89139A","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":"Q4645809$5B606900-5381-47AC-BECC-D1873DD6F03A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5be1e772c7b43052899e2f3979d8211bf7398802","datavalue":{"value":{"entity-type":"item","numeric-id":1155952,"id":"Q1155952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$B5DC076A-0ED9-414C-BDD7-E2F22D03F69B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b78cda30b8bf7bbc1e02364c4dd5fa066a61862","datavalue":{"value":{"entity-type":"item","numeric-id":4279255,"id":"Q4279255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4645809$2E8FA21F-3C2F-4C8D-8848-3A88CE65B071","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b4ea87e1e5dbf358e009a3be4cefaaac5190632a","datavalue":{"value":{"entity-type":"item","numeric-id":4452126,"id":"Q4452126"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"182936fc82b24c71cf36ab2fd89c03e46ac1deee","datavalue":{"value":{"amount":"+0.88692534","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4645809$6F76158D-FD26-47D4-BF4F-24D49BBA9DD4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13c71299e217522f1137d322bf3197d7d1f04f83","datavalue":{"value":{"entity-type":"item","numeric-id":3372480,"id":"Q3372480"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1cf4e5f4bff5e134d0c632e67c21aef3d3bd05d0","datavalue":{"value":{"amount":"+0.88621926","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4645809$24148BC5-6E5D-4D5A-B6CC-45D7F37AC92F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1375df40880817b74ea1f45ffc442d465c6f52e8","datavalue":{"value":{"entity-type":"item","numeric-id":4729320,"id":"Q4729320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bd870d936aff482feb4a4d3132e5e37437b389e3","datavalue":{"value":{"amount":"+0.8829697","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4645809$0340E982-4F31-4B00-8336-38D79C17AAFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8b766d4d7b864501a82e7473e06e5ec450588028","datavalue":{"value":{"entity-type":"item","numeric-id":4941901,"id":"Q4941901"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0c75a0fb60e89165567193e073b5c41c3c0d7945","datavalue":{"value":{"amount":"+0.8807577","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4645809$57F3AAD3-63F7-4458-A942-CCF86072A6E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c29d851e188e9650f65295675c057839464e861a","datavalue":{"value":{"entity-type":"item","numeric-id":1124368,"id":"Q1124368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dc4a986b87ad71f765925c8bc8e33c524230a618","datavalue":{"value":{"amount":"+0.879824","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4645809$2CFDD62F-46C6-496F-9521-BE02B893141C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"80c245a5a4a8d45e73d7e71bfd1127978c47c288","datavalue":{"value":{"entity-type":"item","numeric-id":3455064,"id":"Q3455064"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"bfd9df4d00b1e6b42cc56775e7713870b4f44110","datavalue":{"value":{"amount":"+0.87814534","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4645809$6C75F5DD-F8FB-46DD-B6F4-2AC18E3D9D2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6ee587041bd51b390588853fbdc48e5ebdfa9d1d","datavalue":{"value":{"entity-type":"item","numeric-id":4267721,"id":"Q4267721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d12fc0be68f8a2821fbd3e66b16c623b3f6d598f","datavalue":{"value":{"amount":"+0.872368","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q4645809$805AA0FF-BCC6-4709-BFCA-31E5D6206DE8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4645809","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4645809"}}}}}