{"entities":{"Q3067474":{"pageid":3078190,"ns":120,"title":"Item:Q3067474","lastrevid":51169790,"modified":"2026-01-17T01:34:14Z","type":"item","id":"Q3067474","labels":{"en":{"language":"en","value":"Program calculation in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5839827"}},"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":"Q3067474$F5BCECEE-E532-4787-9697-24116673DB5A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"18840074109d1ae94c5e3790d597057891fcdcc6","datavalue":{"value":{"text":"Program Calculation in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3067474$251CFEAD-A188-4553-83B3-E1D8F005A9E4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0c686f4b4416dd4de2ee58a8ebd9e618c7be7026","datavalue":{"value":"1308.68049","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067474$62A77A44-3233-4739-AAE1-0A55634B63D0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8f3f4d3ebd52c275fce7b3159d7c1d62d12f4c9b","datavalue":{"value":"10.1007/978-3-642-17796-5_10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067474$AB475470-A4B7-40E8-A5AC-8A8670F2E4F2","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5e140591002962188ab525bdb99cf1a6af2817ec","datavalue":{"value":{"entity-type":"item","numeric-id":2879256,"id":"Q2879256"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$9692E5F2-14E5-4479-ACE7-0770116ECE4C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"20262fd99a0096946ca41e5051e1c5352b288570","datavalue":{"value":{"entity-type":"item","numeric-id":702008,"id":"Q702008"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$DF11CD38-DA60-40A3-BE1D-D1DA3344F32E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"bc2dc96fcf8076e448d479ac51b4ccbc7738d2bd","datavalue":{"value":{"entity-type":"item","numeric-id":756402,"id":"Q756402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$A5E04CD0-DFA6-456A-8F70-1C995CF7930E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"264b843063617555d5bcb94bb0f27d02ee5d26de","datavalue":{"value":{"entity-type":"item","numeric-id":542003,"id":"Q542003"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$82EB1EFE-4566-4742-AF7B-5BCF7DDB9ABD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"41523071f7928e35d0476c616da8429088b7716c","datavalue":{"value":{"entity-type":"item","numeric-id":1566917,"id":"Q1566917"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$44A4BD59-1DA3-4869-8249-87A78D548AC9","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"61858cb81e4b5eb34d2de9199633f44c2ecae313","datavalue":{"value":{"entity-type":"item","numeric-id":2996122,"id":"Q2996122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$68A7D0AC-03A6-422B-A64B-2D0FC7534E94","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"3832aa8c4413a9f491fedd54c1d4e68094c46118","datavalue":{"value":{"time":"+2011-01-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3067474$9F15D9D5-4FD9-47E9-9C9E-BB297A40F7E7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067474$6DFB6581-F395-4D56-8614-9B71FED93911","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067474$034FEDFD-9B61-497E-B569-03BF3D6C84EA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"315a8bc73750ac4d579a3ce05484354de401d2c0","datavalue":{"value":"5839827","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067474$C4CF3F01-ECD1-4483-893F-1C72342C3B09","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$A768137F-74AD-4BA9-8BAA-73816189B900","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9db81755b8583ee717e753dd02789b0672cce84d","datavalue":{"value":{"entity-type":"item","numeric-id":21811,"id":"Q21811"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$AF89D483-CA12-4175-AC08-C16579D4FFD4","rank":"normal"},{"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":"Q3067474$FB08DEA4-B6CD-4B65-8056-57E65EF4F1ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e41927344b9397ba2eb05288d661d38c0f0d55a6","datavalue":{"value":{"entity-type":"item","numeric-id":21665,"id":"Q21665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$DF652F40-3194-4414-9C20-61B0A5621C05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e74e65aea50b572ed5cc320d9d0d7a2d70ec494a","datavalue":{"value":{"entity-type":"item","numeric-id":21666,"id":"Q21666"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$3331ABE8-1E7B-4CDB-B39F-CA35E7DB4D9D","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":"Q3067474$27B79490-5C3B-4242-AFF3-85E5B186ACC8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"399b262a8b23c50c5661321fc02f0c39c804f98b","datavalue":{"value":"https://doi.org/10.1007/978-3-642-17796-5_10","type":"string"},"datatype":"url"},"type":"statement","id":"Q3067474$09DB0417-D23B-4D58-BE84-5BB0C839C1C1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"09ffe7658e079114001a069389106365a45a44ed","datavalue":{"value":"W1605536043","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3067474$3FBD991C-2652-4B58-858D-E54E649827C8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"992009231a3ccf90d1f1c83b557e5dfa4622a42d","datavalue":{"value":{"entity-type":"item","numeric-id":921907,"id":"Q921907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$522BBC75-20C9-432D-BAFF-E6196120CC9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"825ab4c172520052e5230110b703709aa8296785","datavalue":{"value":{"entity-type":"item","numeric-id":4885873,"id":"Q4885873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$FDC21485-D885-4FA6-967E-B9CEE52D64C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e72d3481d690e4c10cdc05b7d6ad88162db034f","datavalue":{"value":{"entity-type":"item","numeric-id":4286530,"id":"Q4286530"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$451F374F-F880-4D80-9563-CE267B227BC2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2ac1544b077df7474ecffe72213b1e03f845ec1d","datavalue":{"value":{"entity-type":"item","numeric-id":2766781,"id":"Q2766781"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$F245F40A-7892-480B-9FF0-D62FFADC5C82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ff7181965704e473c064c7d95f9f7f0b397f93f","datavalue":{"value":{"entity-type":"item","numeric-id":3543665,"id":"Q3543665"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$0EC93814-35F9-4CDD-AA25-82F6C0F214AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4acd72c1e9e1c1e1affed03542de8df1198fdc8","datavalue":{"value":{"entity-type":"item","numeric-id":2456575,"id":"Q2456575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$9AAD0879-61F3-462B-9F64-93186043E881","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0bdd715b1026d1cb98b08aebff75dd42a415013","datavalue":{"value":{"entity-type":"item","numeric-id":3644935,"id":"Q3644935"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$1C443208-4CF2-4E61-9CE6-1E89303E9600","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b327cf916e5c8f52b90b371017428a40a2b3f26d","datavalue":{"value":{"entity-type":"item","numeric-id":5348900,"id":"Q5348900"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$8638A64E-2353-4542-B75F-AFDA66BECC31","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2cfd356224155dbd75db29249481baba3510e2a8","datavalue":{"value":{"entity-type":"item","numeric-id":5394302,"id":"Q5394302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$5B87D8F2-9AB9-41F4-A6D1-8B59782A62F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1cb314be56584c4a3b78c42d4c6a1e8e149e010","datavalue":{"value":{"entity-type":"item","numeric-id":3649136,"id":"Q3649136"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$419009D2-B627-49AC-A7B2-B014DA9ACFED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9b06809062082b8f9f5dbc080e3987837376fa3d","datavalue":{"value":{"entity-type":"item","numeric-id":3499750,"id":"Q3499750"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3067474$93F69BDA-8ED7-4BAA-9309-D3A3FFC10C85","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"77217dc2085b0609e7fd5b1db191a64d2ac5718c","datavalue":{"value":{"entity-type":"item","numeric-id":1322847,"id":"Q1322847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"50dd105e517081f59d35b5a5b654ed157e8beb76","datavalue":{"value":{"amount":"+0.7406154274940491","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":"Q3067474$1337769B-AE80-4B13-8640-47C14BFA5C0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9564fbc26aa84919584d31b80771f8b6cda49a26","datavalue":{"value":{"entity-type":"item","numeric-id":3075245,"id":"Q3075245"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7ae1d19567fd63eae10042615fecb9713657720e","datavalue":{"value":{"amount":"+0.7406151294708252","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":"Q3067474$C3C01100-1EC1-4406-9DB6-356886E40B96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"714e15e5a2ba4fff06e9121fed38d3236869a4fd","datavalue":{"value":{"entity-type":"item","numeric-id":1267035,"id":"Q1267035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"46dd4e659d43e26eac6bec670aed9e8cf9c5a738","datavalue":{"value":{"amount":"+0.7367351651191711","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":"Q3067474$FE55A214-84CF-442C-9CC1-19466E7FC41B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e26c3ee28b2edb7374449f2f1032135d4fba7d2a","datavalue":{"value":{"entity-type":"item","numeric-id":2798255,"id":"Q2798255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fcab55ea0f7e268521ff0ac151961bada5590b4a","datavalue":{"value":{"amount":"+0.7321149706840515","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":"Q3067474$690CCB07-B808-4035-B114-E5F977DD4BA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5d5d3a9bfaa35aeb9a6c1d64c9f4dc2c86ed3ca4","datavalue":{"value":{"entity-type":"item","numeric-id":4357063,"id":"Q4357063"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"24b46d71c2dac5e3315c48ffcfb3703d978bdd07","datavalue":{"value":{"amount":"+0.7243403792381287","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":"Q3067474$631A92E7-0792-4469-ABCB-160D739BA7A5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3067474","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3067474"}}}}}