{"entities":{"Q4340418":{"pageid":6370018,"ns":120,"title":"Item:Q4340418","lastrevid":46556067,"modified":"2025-12-25T00:51:07Z","type":"item","id":"Q4340418","labels":{"en":{"language":"en","value":"Mechanizing coinduction and corecursion in higher-order logic"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 1019357"}},"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":"Q4340418$3A773AC8-D6CE-439A-B4D9-24CF3C5BC449","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"40a96c2b84ad1dc9431c3e0109afafd6af9da149","datavalue":{"value":{"text":"Mechanizing coinduction and corecursion in higher-order logic","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4340418$22B92FAB-6B41-4375-9C59-29832ED16C91","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"5add5a1ce24caa9e8d9023bcd4f16be8f9aac405","datavalue":{"value":"0878.68111","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4340418$F450FD70-FF41-49AE-B9D7-06B45E28A6E0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7e2dfb5d8700e631835334f9dc71e9b98ed5a53b","datavalue":{"value":{"time":"+1997-12-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4340418$ACD079FF-9841-4B2D-A0FB-3159CF0C9075","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a8026c0a2fe76918c10d4630372590d3408f599c","datavalue":{"value":"https://www.repository.cam.ac.uk/handle/1810/276436","type":"string"},"datatype":"url"},"type":"statement","id":"Q4340418$D2747DAC-A984-4EB7-8576-9FE7C1F25D72","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4340418$CFC49045-517F-45B9-82D7-B29E68B5E46C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4340418$F35352D6-DB7D-43C0-8383-38EF78F2ACC8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4340418$27A91007-1EE8-4E69-BCB1-DF01E132A246","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4340418$ECF9E13B-162B-4506-B5D1-C1C07D5EEB35","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2adb5483c53ba7ee8395209949e90260aba54cb9","datavalue":{"value":"1019357","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4340418$C44CC690-3A12-4EA9-862A-653894A3DEDC","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4340418$0344746E-3FD2-41B1-84AA-154C845D169A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q4340418$D8B7D13D-7A7E-4A49-999B-B64116669911","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"cb5dfbdfa6d8a2070a67ff948fb8abd387eda36e","datavalue":{"value":{"entity-type":"item","numeric-id":352969,"id":"Q352969"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4340418$0EC2B433-453E-46D9-B676-CA6894F6FEC5","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9c40cf9a35904f638a7cabef2bc178bad46391f7","datavalue":{"value":{"entity-type":"item","numeric-id":13717,"id":"Q13717"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4340418$32F8A370-A6CD-48B3-8EC1-8F543DB390DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"aca41f313ec935c6c7a90dad170b49859b6fac14","datavalue":{"value":{"entity-type":"item","numeric-id":17120,"id":"Q17120"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4340418$062CF447-7D1D-46BD-8BB7-4277C826CC45","rank":"normal"},{"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":"Q4340418$145EC3E4-B4EF-4FA2-AF30-E61ADD10B01F","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":"Q4340418$BBC2F688-F30F-48E9-A8E2-BDC5078D3736","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"8c554f6faa63812da42ffb21ba4a9d586377f06d","datavalue":{"value":"W2053068669","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4340418$7B4A7860-4C30-4EF1-98B9-BDB6FC1189DA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"fe7e30d2f6ce0c2c07625c7e5c3ab212a9b6acd2","datavalue":{"value":"10.1093/LOGCOM/7.2.175","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4340418$68FF2F53-51A5-4BDC-AB83-447C0FC74A4F","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"9e6aedf3faf6964e0bbb1663882629f007284aa9","datavalue":{"value":{"entity-type":"item","numeric-id":2983390,"id":"Q2983390"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4340418$3A2471C6-C9EB-4652-B379-F75FC8DF0DC8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5c843f37bf1149130399feda41a62effd30beec5","datavalue":{"value":{"entity-type":"item","numeric-id":1687535,"id":"Q1687535"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"def6dea372791fdb980927914e1ccae9e16f03c7","datavalue":{"value":{"amount":"+0.820885419845581","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":"Q4340418$314A52E9-2B6C-4FD7-AEF5-ACB000DBFD1D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7a940f134dd0a9eb9d1b7f05231f4516f87efb52","datavalue":{"value":{"entity-type":"item","numeric-id":4945204,"id":"Q4945204"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"635d98f0526c74fbfbbe8d913efbc193d9ac1179","datavalue":{"value":{"amount":"+0.7911578416824341","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":"Q4340418$45040116-4AB3-47D9-A191-E1758C7C3745","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"523f04cb2e34b987f8f0638ca56920c6298ac76b","datavalue":{"value":{"entity-type":"item","numeric-id":5210768,"id":"Q5210768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"32856ea07e6048b34f4ce8485a946985e6ba2bfa","datavalue":{"value":{"amount":"+0.7744548320770264","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":"Q4340418$3D32790D-9871-4B84-8FD2-D342EDC04329","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24fe603be126cf3667eea9dd66064ca9076cdc76","datavalue":{"value":{"entity-type":"item","numeric-id":1904402,"id":"Q1904402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b189a45bfd6fe2594fe200b5b5dec2d4e615e50","datavalue":{"value":{"amount":"+0.7555105090141296","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":"Q4340418$7890F5AF-6C1D-4C5D-AA22-F1449AFAF1CC","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4340418","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4340418"}}}}}