{"entities":{"Q2945637":{"pageid":2956357,"ns":120,"title":"Item:Q2945637","lastrevid":44758431,"modified":"2025-11-25T20:31:22Z","type":"item","id":"Q2945637","labels":{"en":{"language":"en","value":"Refinement to Imperative/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6481868"}},"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":"Q2945637$F4C6300B-38BC-4419-BA44-11F30791712D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fe3e69a82bb4aa07438e5797fe0a49c6fd07ae2e","datavalue":{"value":{"text":"Refinement to Imperative/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2945637$7449A357-3E19-4061-AEA1-6AE9A02ADC73","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"efca43f2a94d8f28d8db9d668a2ce849e932176e","datavalue":{"value":"1465.68290","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945637$69ED4E19-9AD5-4510-9B84-DC7D1FE6DBC2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"47e3820237e642f68daeb2894ea4100ed6607fdd","datavalue":{"value":"10.1007/978-3-319-22102-1_17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945637$BAFD7F0D-ECDD-4B40-9D67-D41FC1CAF231","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b8e4be225a6094490d6530fbb2f56929f5bbbcf0","datavalue":{"value":{"entity-type":"item","numeric-id":682349,"id":"Q682349"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$1316F7AD-BE9D-4130-8A60-E895C16C653D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$A033CE16-DECD-4E9B-9F69-B390BD7AAEA6","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ece460bc202bb4ec344b5d620998e472753b138b","datavalue":{"value":{"time":"+2015-09-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":"Q2945637$C886742E-7C2B-46EE-97EA-9B1329E0FF7D","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"761aa19cc64fe046a4fed508e2e4da3ce5280569","datavalue":{"value":"https://www.research.manchester.ac.uk/portal/en/publications/refinement-to-imperative-hol(3de7ca0b-1d46-4597-8f1b-378239c2c10d).html","type":"string"},"datatype":"url"},"type":"statement","id":"Q2945637$F7A65198-181F-4BC9-9D3E-E633D86906EC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945637$90195DE0-DCFA-47B3-8F27-D67929FFDA0A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945637$0A51E5A2-5B3B-4ACF-9AEF-80C9FAF14564","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945637$570566C8-BF37-4DF3-9E53-E670BA19E40C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1bcdc2a107fd2414d151e8610f3471a8784e75bf","datavalue":{"value":"68W01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945637$C98A6582-DA4E-45A3-8895-0E5986235689","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"797a03a6e122957b37decd153e39f03e2ff03326","datavalue":{"value":"6481868","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945637$D8443254-0A73-4754-9911-BF7EFD6ED38C","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":"Q2945637$F9D1C53B-7985-487D-B446-9C476BF4BC26","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$462E51CD-CD97-4AB4-AD46-5AC4B57580AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"36775e519793d9171689cd087c9a00c3267ecefa","datavalue":{"value":{"entity-type":"item","numeric-id":21794,"id":"Q21794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$9D873F46-EBB1-463E-B833-77993D08B790","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4f930b95045a1000563a1c7315d8b3659e0c990e","datavalue":{"value":{"entity-type":"item","numeric-id":26832,"id":"Q26832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$33DF5AEB-3676-4214-BA96-4E0D65345BE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"665b81d9c0f077e3e09c3e4e80080780b437ea70","datavalue":{"value":{"entity-type":"item","numeric-id":40264,"id":"Q40264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$1EA5AA36-85F0-470C-A60F-DC940C2C13C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6d082feafa45d8fd2af5638ac3cc0080de90d3ac","datavalue":{"value":{"entity-type":"item","numeric-id":40263,"id":"Q40263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$45C6B059-68D4-4E3E-B12B-8213C17CD39D","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":"Q2945637$45D3070E-72FA-4C90-BAC0-1B10351A15A0","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":"Q2945637$FD0FBF80-91A0-4E59-8451-1BE346FB5079","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"1224a5f58a0912d37b2c73206507e6604312613b","datavalue":{"value":"W1955004327","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945637$B18BAC61-C44B-4198-9886-387FA1090014","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"91b08ff1b0d4539c99f6902ec8427b7b8b6cea46","datavalue":{"value":{"entity-type":"item","numeric-id":5276151,"id":"Q5276151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$867AFC08-A579-4C70-ADE2-A527DFAFC3E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a1ce762817aa67ba84d34579fd3b9060a2c653","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$18AECDDF-44AC-4CED-A830-B31E96256B46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0092ca3b21f3f9cb157bf2001ff878cfeab4655","datavalue":{"value":{"entity-type":"item","numeric-id":5261525,"id":"Q5261525"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$9543B929-8386-490B-A485-E7E7066369D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3343c3ecaf29b3d00ed730793fb135803dd0ca2f","datavalue":{"value":{"entity-type":"item","numeric-id":5176992,"id":"Q5176992"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$1B3FC036-82F1-4A94-BBCE-2244B8C93BD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81006327d72d2859034c6eecc92705ccc5770eba","datavalue":{"value":{"entity-type":"item","numeric-id":3377461,"id":"Q3377461"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$B7EFE662-0113-4001-87C0-B62E7B1D22B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"31067e58485990e94b288d36b9237062670ad8fb","datavalue":{"value":{"entity-type":"item","numeric-id":4356435,"id":"Q4356435"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$D917EF48-D45C-4AD9-B9C2-CFBD604B86D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88fbfcea2166cf55628dc74bb062db5b5b011195","datavalue":{"value":{"entity-type":"item","numeric-id":2914753,"id":"Q2914753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$77DB36BA-C881-4267-B1CA-6673CC2F3987","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22a5a326924c9f9f3cf0f5061fb0ff950ccfad0d","datavalue":{"value":{"entity-type":"item","numeric-id":5747660,"id":"Q5747660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$7585DCD7-7542-4EBE-91EE-D8FEED58D027","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7f766bae7bb1dc745731294a8b2405f79150a41","datavalue":{"value":{"entity-type":"item","numeric-id":2914741,"id":"Q2914741"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$8E150D7B-9D23-4CC6-9B15-161CB53B7318","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"50b0bfaa5604fbbf1607bb7e54efdd2fee887b49","datavalue":{"value":{"entity-type":"item","numeric-id":5327338,"id":"Q5327338"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$B58EE867-6F93-47FC-9970-113B8D6226E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2235cb100f2692698d1e78c89e440355cd4f7add","datavalue":{"value":{"entity-type":"item","numeric-id":2879261,"id":"Q2879261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$E4966CBE-AC30-4BDA-B959-D3E88B59EA8A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f96080269f1ac57df102d277e6fe30615563ee72","datavalue":{"value":{"entity-type":"item","numeric-id":5178765,"id":"Q5178765"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$9FB06B03-02C1-45CE-9340-F9C749D537B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"829c2fc52e5b12c8e00ff0f0fcc73378436c283b","datavalue":{"value":{"entity-type":"item","numeric-id":5703757,"id":"Q5703757"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945637$CC0A301D-22A6-4155-8C61-7FB9A4F90D5B","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":"fc07f2f74bd4966ca1c8da7f7519d8f8f26e1fd1","datavalue":{"value":{"amount":"+0.9930618","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":"Q2945637$35143AE0-8B2D-40DB-9994-34BE82A391B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0e851c767c872a2c8b708d838a05400c4392ce5e","datavalue":{"value":{"entity-type":"item","numeric-id":4702597,"id":"Q4702597"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"09213fa5a1f74e657d2dafe00b815bd728b1f37d","datavalue":{"value":{"amount":"+0.77448976","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":"Q2945637$671E7E26-056D-4505-A49D-6EAF77D5E257","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1d658af1324e436d1f21251ef5012d1fd9b6cdd5","datavalue":{"value":{"entity-type":"item","numeric-id":2835902,"id":"Q2835902"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"943934a89acd201d4dcd918a2cdce285afe16e76","datavalue":{"value":{"amount":"+0.7702344","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":"Q2945637$3832E766-C555-499D-8E4C-5408580278BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"badab0587d6a86cf23b0e6488e596803e8e7f3fa","datavalue":{"value":{"entity-type":"item","numeric-id":2879242,"id":"Q2879242"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a36199c54ec5b052e7264a457b3e3703536e65f6","datavalue":{"value":{"amount":"+0.7638682","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":"Q2945637$11C68D43-0478-4CB3-BFDF-CC19F39D478F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc34f59ed8e9f7b8abc3b304054cb60be3fbd4eb","datavalue":{"value":{"entity-type":"item","numeric-id":916409,"id":"Q916409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a87e959640bd9a6cb64beb2d2db1037230d159d3","datavalue":{"value":{"amount":"+0.7607618","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":"Q2945637$08603A64-1CA1-42CA-B9EF-FC71764A975D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cdedcfa78b543832264192436362e87b6cf3afa5","datavalue":{"value":{"entity-type":"item","numeric-id":5222694,"id":"Q5222694"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c599a6b8d86c41091069e655e3ee96c777cf0b57","datavalue":{"value":{"amount":"+0.7561663","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":"Q2945637$A1DDD5E3-20CC-4F2D-A4F0-C7C931F8B90C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"01ec202a2cd9162ab8038008edf7a3ed4f1dc404","datavalue":{"value":{"entity-type":"item","numeric-id":5861785,"id":"Q5861785"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f212848089cfd2a543b2ad691b755ee46993d87d","datavalue":{"value":{"amount":"+0.7558783","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":"Q2945637$8349E53E-E59B-4A7E-A8BD-52F4F84DB75C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6b7bf791b9abdae5271151a91243056450d2052f","datavalue":{"value":{"entity-type":"item","numeric-id":4659989,"id":"Q4659989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ff0d901189d16e2423a0785214e540148347ea3a","datavalue":{"value":{"amount":"+0.75266886","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":"Q2945637$C69891B6-D1FC-4921-B948-72D8AD6145A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"819214126c1c94e9b067a06e7484d2b50529a1eb","datavalue":{"value":{"entity-type":"item","numeric-id":4362886,"id":"Q4362886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7718c871a52b51069d5900ffe85c7977132a2ebd","datavalue":{"value":{"amount":"+0.75090855","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":"Q2945637$B098DA35-C7A4-4F56-B8C1-7B123F987650","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2945637","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2945637"}}}}}