{"entities":{"Q3543655":{"pageid":5573559,"ns":120,"title":"Item:Q3543655","lastrevid":50516507,"modified":"2026-01-14T06:35:00Z","type":"item","id":"Q3543655","labels":{"en":{"language":"en","value":"Imperative Functional Programming with Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5378178"}},"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":"Q3543655$7DAA3C6F-C088-45FF-A8FD-1F7E930F3B47","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"565ce74433996090c9396fb60383cde33192df24","datavalue":{"value":{"text":"Imperative Functional Programming with Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3543655$674B2071-B07C-41FC-940B-06E764E573E6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"e125d7de1bb4401106dec11ae06c4aea9a8ec3c6","datavalue":{"value":"1165.68352","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543655$D40778A4-0ACF-40D5-937C-D47E169A694B","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"cbf017be3d5c4d0f04fef97aefd68fb0f399736f","datavalue":{"value":"10.1007/978-3-540-71067-7_14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543655$006EAB58-8B2C-41F2-BF31-9C10DC45FD7A","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":"Q3543655$CAF0E525-C58A-4A68-BF63-B5303A0483AA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9390341f6bd0adb4a80933997da5182af87828a8","datavalue":{"value":{"time":"+2008-12-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3543655$7441D239-5E92-4568-9EDF-54B9A7D9145E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543655$27092C04-0B76-4E7F-A438-6D209BD03949","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543655$70931A3D-A3D0-4B69-8A38-2525A2C428B1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"b8fb94a4817123f3c4959fb83b121c0a45a0c87b","datavalue":{"value":"5378178","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543655$4684FB1A-91DE-4760-97CA-C1ED9FEEF7D2","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":"Q3543655$666D10EB-D4B3-4280-98D9-851F6D35513E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fe5077d712c4f7a91829b6a22ef0e0039cd600ea","datavalue":{"value":{"entity-type":"item","numeric-id":15691,"id":"Q15691"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$6F1B87DA-7FD6-423E-B9CE-AE2E40E146DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d560ad72fd288969b6a46f8ac77d54f6d297bf97","datavalue":{"value":{"entity-type":"item","numeric-id":16796,"id":"Q16796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$20A2E751-2B66-4BF7-8FD8-4C593B115DB0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8449db7d9aaa28101ba7b0de8e98d9c446365070","datavalue":{"value":{"entity-type":"item","numeric-id":13332,"id":"Q13332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$E0961B7C-A383-4EFB-BBFF-1CE06B8F9E94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"602b32d79a3dd12c7713e80fb0597b8ab4375f08","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$2431FE47-A1CB-4B58-94D9-58928D66D511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$8E994C2C-1F6B-4A5C-AFDA-8DFF3F093062","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":"Q3543655$FBFC7865-54AF-4777-9822-295D35E0652E","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6d32858be7a09471e70c358b98161855f629cb3f","datavalue":{"value":"https://doi.org/10.1007/978-3-540-71067-7_14","type":"string"},"datatype":"url"},"type":"statement","id":"Q3543655$082410A4-780F-43A1-830C-9D81EA70AB3F","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d406afc5f405108a459cd6fc6b8fe52af433aef5","datavalue":{"value":"W1522519483","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3543655$F870D0B8-1CF2-40E5-B5B5-FBB92828AAD9","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"22485e2e7f5d751287059d6c89f8749b6a408a20","datavalue":{"value":{"entity-type":"item","numeric-id":5325885,"id":"Q5325885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$B0604B2D-4EE9-48C8-8187-688536492FE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c82348539a9abdb43fbaa5beca3b7e0847dfca6","datavalue":{"value":{"entity-type":"item","numeric-id":5477652,"id":"Q5477652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$5EB1F3C6-7FA3-474B-A406-2B008DE5565F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be2cf1232ac409818cf28b980d37060875f07594","datavalue":{"value":{"entity-type":"item","numeric-id":4736996,"id":"Q4736996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$C0612392-8728-4D9C-A1C2-63CC55A9BC93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"923d9841ebb82ba7564626f46c70dd17455ed552","datavalue":{"value":{"entity-type":"item","numeric-id":4267723,"id":"Q4267723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$50578651-0CAE-40E5-9AA3-66D4837106E6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b09623b25863ff5c40989a5025b9634ea6113fef","datavalue":{"value":{"entity-type":"item","numeric-id":5501458,"id":"Q5501458"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$DE1C7265-C56A-4D60-9778-DDE8FFDFC8C0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5c2de221e3b126781b22b880228fcab371b66f0","datavalue":{"value":{"entity-type":"item","numeric-id":3525155,"id":"Q3525155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$833A4739-0D3A-44D9-B9E8-3ACA499CD6D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8ec976db9fee9bededf233dd7d31c7e9ef2213c8","datavalue":{"value":{"entity-type":"item","numeric-id":5705937,"id":"Q5705937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$A3AE9B33-2620-4710-8907-B9137C260125","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6eb24132ceead7ee6cd48198dc7aa757adff4770","datavalue":{"value":{"entity-type":"item","numeric-id":3523184,"id":"Q3523184"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$4548D27E-C1A7-4D60-97C1-C862A690127A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19d68f92fffaefe72b592d24843b2770631f989c","datavalue":{"value":{"entity-type":"item","numeric-id":3189788,"id":"Q3189788"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$F289B157-988E-4943-B100-009F1AF426D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"271326b3f6ba4699b8b9534f6c64338c8ddd3a50","datavalue":{"value":{"entity-type":"item","numeric-id":1006729,"id":"Q1006729"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3543655$F4A297E8-FC1D-4023-9320-889244318061","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f06ce394d56681f16987829d5518799d1c8091e1","datavalue":{"value":{"entity-type":"item","numeric-id":1739909,"id":"Q1739909"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f9b536b98ecd2e86d91f8e411fd78cb77fd3c3fa","datavalue":{"value":{"amount":"+0.8308098912239075","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":"Q3543655$BE261011-5564-4641-9506-C600BC753890","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2329ac48b709f66aa4e2a0cfdaaaf3d4cea285dd","datavalue":{"value":{"entity-type":"item","numeric-id":5705937,"id":"Q5705937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c581884e66c612e12d0f1b36dcb98e9551427a9b","datavalue":{"value":{"amount":"+0.8274818062782288","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":"Q3543655$5FFBA176-2611-4ECF-82AF-8B4BAC8B7142","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"959be19baa4476667a8bf253e7c26f9c31eafdc1","datavalue":{"value":{"entity-type":"item","numeric-id":2945637,"id":"Q2945637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e85da302289bfb7481c973da36164bc33ddedbe","datavalue":{"value":{"amount":"+0.8263905644416809","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":"Q3543655$6C39EE87-E61C-49E8-8BEB-FC7C3364C960","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f959c7712c196883e995861185c429abdff17384","datavalue":{"value":{"entity-type":"item","numeric-id":4944851,"id":"Q4944851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9f91810a8473f29a726d27443ce441335d58e5f3","datavalue":{"value":{"amount":"+0.7888460159301758","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":"Q3543655$8C3B4075-3AD8-48AF-AD7B-2CFADEA025AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8e4f7550369b8e1b947e819d750997574708bd86","datavalue":{"value":{"entity-type":"item","numeric-id":5900714,"id":"Q5900714"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"06ee45e11d6805073407dad79d62628733ca8888","datavalue":{"value":{"amount":"+0.7796199321746826","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":"Q3543655$E93B58C3-31EB-479E-AF75-9BB2C10A564C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3543655","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3543655"}}}}}