{"entities":{"Q4647582":{"pageid":6677163,"ns":120,"title":"Item:Q4647582","lastrevid":53321237,"modified":"2026-01-24T17:45:07Z","type":"item","id":"Q4647582","labels":{"en":{"language":"en","value":"Circuits as streams in Coq: verification of a sequential multiplier"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7002055"}},"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":"Q4647582$BB632D84-1365-4944-A187-469F9313729B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"06572a365647c25654a0021ac43571b8f70a4e9c","datavalue":{"value":{"text":"Circuits as streams in Coq: Verification of a sequential multiplier","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647582$8A1C0BC4-8E6D-4EA9-8F8C-0F5BD0D019A9","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2276baaf336a0c1f47437a9081964dcb9edfd57f","datavalue":{"value":"1407.68439","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647582$3F59F33C-F921-4F0E-A6D9-460D8FE0FCE5","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"795952e64d1c8e7dc7d9e7f186628267f7f9040a","datavalue":{"value":"10.1007/3-540-61780-9_72","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647582$80EC0E8A-402C-4AC5-AF2A-9047FB94E3BB","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"4bba7ec8861a8ed927cac8194bcfd558f8fc7d3b","datavalue":{"value":{"entity-type":"item","numeric-id":923885,"id":"Q923885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647582$9C707E11-4C51-4761-9A02-0B317F847365","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":"Q4647582$19CB1D89-01D1-4000-818D-F3D5604ADFBF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647582$32ADE498-7794-454F-AD80-EC95DE9BEDD6","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b58a5a80209cb8a9cc8fa4adcc32294cbb8e324b","datavalue":{"value":"https://hal-lara.archives-ouvertes.fr/hal-02101845/file/RR1995-16.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647582$64408669-8146-45FF-BF66-F7568C188702","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647582$0CC9BDBC-9971-44DB-BB20-8385FA11D4DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647582$54A75B67-EE62-4496-B031-5109420EC07D","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"dd9ac7c4184d40884bf13d03612cae436af35f91","datavalue":{"value":"7002055","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647582$54B34442-5B06-41F9-97FC-08CB779D258C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"39810ec381ba48fb5861c168391fa7d328efd8b1","datavalue":{"value":"higher-order logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647582$4932C96A-3B1A-4437-A643-A69C3627DB15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e79a5f80570e401200acdc85407f2ef3675aeec4","datavalue":{"value":"sequential circuit","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647582$38ACB78A-E07E-4F9D-816F-63573DF16757","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e3795c0a3853f795b0cb16bdc5c89a3cceb87864","datavalue":{"value":"sequential multiplier","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647582$D3FFE40C-67F5-4C85-9416-8EB291CEEEBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9088d36eb6cc3697f6f61e23bf3a078d7f5fb0ca","datavalue":{"value":"multiplier circuit","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647582$317607FC-74BB-469B-AA31-A0AF88684449","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac52900f9c775a1c2e9b77521a060cf4681ca7f4","datavalue":{"value":"hardware verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647582$E028F7DF-04B9-4BA8-9179-6E566077221F","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":"Q4647582$52C49575-D323-4F43-B9BC-CD99AF4BF77E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2b02b46847f3d7e3a5825b9484a88607b98dbd14","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647582$2817A46E-FB1B-4579-A91B-112968298390","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":"Q4647582$8E5E9839-1EF1-4674-ACB4-E4792D839860","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2e07b63a7544a6d7c83390f82ddae368b77e124c","datavalue":{"value":{"entity-type":"item","numeric-id":19570,"id":"Q19570"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647582$035AFF03-60E9-4598-9419-C46702352794","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":"Q4647582$6C07158C-DA9F-4C1A-987F-48418CD1573E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"d5a6349fcd1f07715bba2fba1996a7280976fd79","datavalue":{"value":"W1536384265","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647582$C95771CA-8248-4A66-8B68-2CA0BA187851","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8124e2aa86067094dab23bb14b8dadf2e19d522b","datavalue":{"value":{"entity-type":"item","numeric-id":3894958,"id":"Q3894958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647582$6ECE4A8C-8479-4811-86AE-BA292F90A6B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0aad2711eb9c64a58dada485191047b8af29959d","datavalue":{"value":{"entity-type":"item","numeric-id":4040283,"id":"Q4040283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647582$F7DD153C-3F7F-446B-AC16-BD52992EA198","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d42e5dea39186928a0c58c53a8feccbddaca803e","datavalue":{"value":{"entity-type":"item","numeric-id":1764432,"id":"Q1764432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647582$93F34ED9-4F38-4466-80C5-75ED456B7744","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53272d2173db9c6e31a2df5def7f3ca8e8e0c9bb","datavalue":{"value":{"entity-type":"item","numeric-id":3753927,"id":"Q3753927"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647582$38494C3E-1879-4099-91BF-6FDA14D3255C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"df6d745c28f41f3f6887e89cc1ca892988e70309","datavalue":{"value":{"entity-type":"item","numeric-id":5287513,"id":"Q5287513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647582$78FA2B15-DD0B-46D2-A65C-6B3B54999E62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c14d3c940a5cb5f7068f644a997c203fcc785357","datavalue":{"value":{"entity-type":"item","numeric-id":3784044,"id":"Q3784044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647582$45AB3AEF-D40F-43A0-BC65-A69FCF6CBAD3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"481f5099a98f54fe4780c855a7f8b1692d0b248c","datavalue":{"value":{"entity-type":"item","numeric-id":5096255,"id":"Q5096255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647582$D4B3F623-23A6-435C-A6E6-BC344C3E0A27","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3759b7d7dc516dbd11ddc44d79565c29c01c078","datavalue":{"value":{"entity-type":"item","numeric-id":1764432,"id":"Q1764432"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"eca19ae2d61fc27f846e9a4660adab6897d28a58","datavalue":{"value":{"amount":"+0.8264175653457642","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":"Q4647582$F7964AB0-4C53-497A-B598-D075B000CAAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d70d5ce8b63a6d88c2164ea8975126b43fca81b","datavalue":{"value":{"entity-type":"item","numeric-id":3100217,"id":"Q3100217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c75301e4ed2bc2eedb0d610fb7808a11c7ca9d36","datavalue":{"value":{"amount":"+0.8004662990570068","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":"Q4647582$D64F4EFF-B8C3-4CAC-A397-74C2D9037FA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a88d5c4105bd54b2dc07fa9bae0d1279569ce522","datavalue":{"value":{"entity-type":"item","numeric-id":3612501,"id":"Q3612501"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6878b766a7ff0513f8d75734a6ef7ab1decb7819","datavalue":{"value":{"amount":"+0.740847647190094","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":"Q4647582$B59236A6-41F1-4A39-9BB9-565A6E5608E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"15228657d37a97a642337cdf95beff22b06dcd3b","datavalue":{"value":{"entity-type":"item","numeric-id":3535611,"id":"Q3535611"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f5ec1e092b8769be8c87248784fb9fb4f86c2efd","datavalue":{"value":{"amount":"+0.7348704934120178","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":"Q4647582$2636E5C0-B896-4F07-BC26-85B899FE5FFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"085d01fd3d5b64326f9bbba67b5309731c5b996b","datavalue":{"value":{"entity-type":"item","numeric-id":1856145,"id":"Q1856145"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4dbe9617d578369497013caffb649bdf077892f9","datavalue":{"value":{"amount":"+0.7331637740135193","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":"Q4647582$046EF879-8E45-4833-B60A-95322EB6F1C1","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647582","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647582"}}}}}