{"entities":{"Q928671":{"pageid":930519,"ns":120,"title":"Item:Q928671","lastrevid":65442870,"modified":"2026-04-12T02:38:01Z","type":"item","id":"Q928671","labels":{"en":{"language":"en","value":"Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5287723"}},"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":"Q928671$FFBF21B7-7DF1-4EBC-A3EF-A57878A3BCC3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e3f34930c27f2bd8b0fabf65b234db2ceea5edcb","datavalue":{"value":{"text":"Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q928671$386B4638-5011-48A3-9CDA-8F6A33E88B28","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"778da70887989a399c86f615f03d547fbdd4bd97","datavalue":{"value":"1140.68491","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928671$E73D278B-D34F-4660-B47F-4608BBF0C4C7","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"14de6399ed68b8e9b6c4461a695ee55ff6b12be4","datavalue":{"value":{"entity-type":"item","numeric-id":928669,"id":"Q928669"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$7BAA86E4-5049-402A-8C4E-3B638AFF42A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"7b7ef19f407c37a1344dec34df08d6a64a61774f","datavalue":{"value":{"entity-type":"item","numeric-id":928670,"id":"Q928670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$73B49CEA-46DD-4661-849A-E10A8F87684D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4b1e35c1c4bff0a8e8e775e8600e2e952b118ae","datavalue":{"value":{"entity-type":"item","numeric-id":848738,"id":"Q848738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$E32C1CA3-5304-4864-AF5A-6A0C2F8B6FA9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$B712C68C-0AED-45C8-8A15-660492490A54","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f1c0b93a352a714c61ccd46766a52600d36f8c2","datavalue":{"value":{"time":"+2008-06-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":"Q928671$F4B165D5-6E6E-462B-94B1-1E8755BD0F81","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"543a1f0f842acc18aed9eb78339cafc558e6f613","datavalue":{"value":"https://hal.inria.fr/inria-00289709/file/parallel-move.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q928671$5154907A-2EA1-4371-85ED-2B257FEC86EE","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928671$A5C8EB07-F9A0-4706-9425-3047B8A341AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3affb2aa66be15f2a63c60d2aaa92bd143e6d46","datavalue":{"value":"68N20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928671$1347564A-76E2-4B37-BFB1-72E3187E5E04","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928671$EE615E80-E0D3-4B82-BF1F-AE9C47A75198","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"74a1927827fb739d9b86be2602b146fb69fe6923","datavalue":{"value":"5287723","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928671$64A7693C-2A52-4007-B12B-A2937132CD5A","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"27aa27636558b175ae09881186916336852a9657","datavalue":{"value":"Parallel move","type":"string"},"datatype":"string"},"type":"statement","id":"Q928671$3F9CDA99-A76B-434A-A370-B845DC58C510","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a56db23d291c315c558cccd230ffccd262188109","datavalue":{"value":"Parallel assignment","type":"string"},"datatype":"string"},"type":"statement","id":"Q928671$70D99E44-4EFB-4F1E-BDE5-144B7C9A8EE2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69e0caff5c0a91fb198655de720cf8460d53d094","datavalue":{"value":"Compilation","type":"string"},"datatype":"string"},"type":"statement","id":"Q928671$25B4EC50-A0EA-4C6E-9E25-85E10F6FF455","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"74f56ce60afd9376ba8f3f9f82181cbcad9eda4e","datavalue":{"value":"Compiler correctness","type":"string"},"datatype":"string"},"type":"statement","id":"Q928671$C0D33C58-FE29-42E1-9A8F-2934BD956A27","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"98456cd4cdf0db037b678749018452921ff9260b","datavalue":{"value":"Coq proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q928671$16DA6901-9C9A-4440-84EC-9C019F541539","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":"Q928671$7B9AD961-46B6-43CB-8DEE-241DBFB841A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"73bf07fb0985efe0166024eb806e5cf2244671a5","datavalue":{"value":{"entity-type":"item","numeric-id":18489,"id":"Q18489"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$A09D06AE-BBA5-43C0-9E11-D185763F7C69","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":"Q928671$B3836998-0C57-4439-814F-62ACE8D8E903","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"9f0f7f6859bdf5fe76399be3d95d7974f438ceaf","datavalue":{"value":"W2118598235","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928671$B8707833-643A-4028-93F5-F5F7B65B4DED","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad38e0ef5109c872fd15da36ed5bb76b94d70ec6","datavalue":{"value":{"entity-type":"item","numeric-id":3434629,"id":"Q3434629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$71B337F7-C919-4926-B228-C5D4F21489BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$38677442-81F6-41E2-B0F6-7204D838B122","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48954ed389c940d6f18707b42187ed03f7c9e725","datavalue":{"value":{"entity-type":"item","numeric-id":5898173,"id":"Q5898173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$94E50666-EB54-4E97-83E1-29A26F3DE266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c24d98fe8151a7ee984475d5ecd61101306ad23e","datavalue":{"value":{"entity-type":"item","numeric-id":4461768,"id":"Q4461768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$BB3E2613-3182-46BF-BCCD-B0FB38178388","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f2f77790f3de0e7a5198a8f1c64a8023dd2bee09","datavalue":{"value":{"entity-type":"item","numeric-id":5348912,"id":"Q5348912"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$6F6693E4-417D-47F8-B54A-4084FCB67961","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2bb1812a83c3a4aee25d6a67b2527c143aea9ae4","datavalue":{"value":{"entity-type":"item","numeric-id":4435471,"id":"Q4435471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$7355E66E-A1E9-4696-BEA4-E6F2C32707BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9acfd539e0a707af284bb7b5ed5e9f2fadb25dff","datavalue":{"value":{"entity-type":"item","numeric-id":1393119,"id":"Q1393119"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$6A179543-54A8-47EF-8122-0463A78FFEA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"39c91241d48f82b5bfe2fb3dd4d4e7f679dbb120","datavalue":{"value":{"entity-type":"item","numeric-id":3668820,"id":"Q3668820"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q928671$05DEE86C-B5D1-437F-A580-EB0111C45FA3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"7401825cd855356a2519e767c155b6bcb01cedfa","datavalue":{"value":"10.1007/S10817-007-9096-8","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q928671$EC8F1A7A-CE6A-4301-A117-33A801639C3B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7c1b14ec371401427672b91fc35789315ae30462","datavalue":{"value":{"entity-type":"item","numeric-id":2871836,"id":"Q2871836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0b30c85374b11a12289edfe333addfb744486087","datavalue":{"value":{"amount":"+0.86909074","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":"Q928671$035E6E62-D3A8-4838-96C9-1AE90BA69EC0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"700510cf22a02be31071f4d2f4625b4668bc1ee0","datavalue":{"value":{"entity-type":"item","numeric-id":2879257,"id":"Q2879257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2ccea0234bcc7eda94dead0e356d25a91e812ff1","datavalue":{"value":{"amount":"+0.860146","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":"Q928671$52DBDA12-CD0E-4AB9-ACD4-0ED687273BF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36258116623966e4f90ed7ba6a441e7310ba87bc","datavalue":{"value":{"entity-type":"item","numeric-id":2152300,"id":"Q2152300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b0c31d6a5d5a0806ab3dc0dfc58ed32d8351f0a4","datavalue":{"value":{"amount":"+0.8574368","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":"Q928671$9C72CD35-C264-4C53-BD63-8C14A540B87C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"150ae9338299f5e5f08685b26bddf8075ea15403","datavalue":{"value":{"entity-type":"item","numeric-id":2035655,"id":"Q2035655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"1e8a47bd95e220cc0d4b01d12ce5b058981ce255","datavalue":{"value":{"amount":"+0.85649294","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":"Q928671$CB1C621D-86AF-4133-B89C-889A22A35E1F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d13d0356133a0244fa0313c0138d1701b208a204","datavalue":{"value":{"entity-type":"item","numeric-id":3347266,"id":"Q3347266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"899d2b364e58d9eac4bcfeed3954359b1f926ccd","datavalue":{"value":{"amount":"+0.8533474","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":"Q928671$3448F644-DE95-4F98-9E71-4EB68BC1E359","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2b23862c78a7611a24576b4814adbb2c63c67740","datavalue":{"value":{"entity-type":"item","numeric-id":5421199,"id":"Q5421199"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b7ce1822d7f45c834350edfeddbdf2e3838484ba","datavalue":{"value":{"amount":"+0.8455167","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":"Q928671$483228AF-E613-4888-8B38-04A5EF1DD872","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4d909f65fd81e7f2c38999ed7dd31b8f28548fec","datavalue":{"value":{"entity-type":"item","numeric-id":2798271,"id":"Q2798271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6b85c7f8b5bb14e68dbe1672c83909b84de4a3b5","datavalue":{"value":{"amount":"+0.8445925","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":"Q928671$59D82F7B-AD1A-436C-92A8-89013DFBD429","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6a1ea13f2a3f0cfb8cab0079f201857881dc2dc4","datavalue":{"value":{"entity-type":"item","numeric-id":2754056,"id":"Q2754056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"279d617576037d694935927a5f24903203582ce6","datavalue":{"value":{"amount":"+0.8434096","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":"Q928671$0A47A0AD-3FA8-4114-B0EB-CAF52B3B6155","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85fe0cfba50ab81867fa509e16f2465ae8978f99","datavalue":{"value":{"entity-type":"item","numeric-id":4484330,"id":"Q4484330"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"37d75e52040f97e593cab9b047adaf87a3a17e3c","datavalue":{"value":{"amount":"+0.84218884","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":"Q928671$74A5F17B-6190-4424-B4CC-A9E59076B09B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Tilting_at_windmills_with_Coq:_Formal_verification_of_a_compilation_algorithm_for_parallel_moves"}}}}}