{"entities":{"Q2798255":{"pageid":2808993,"ns":120,"title":"Item:Q2798255","lastrevid":83528183,"modified":"2026-05-07T08:37:45Z","type":"item","id":"Q2798255","labels":{"en":{"language":"en","value":"From proposition to program. Embedding the refinement calculus in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6562502"}},"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":"Q2798255$B7F4048A-A101-460E-A33A-BC8EC4B2E9D7","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"f2b37181eb0e924008a16528a275219f4c820d9c","datavalue":{"value":{"text":"From Proposition to Program","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2798255$E56A9C06-924B-44B5-98B3-709BB76CC084","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"82a979676d623637a69d7af94818c60674bfeff7","datavalue":{"value":"1475.68458","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2798255$E37D3DC5-D1F2-4E31-825E-53C12C5AF90E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"75db2dc67b8c7bc5ec3fefc633c5931294d70af7","datavalue":{"value":"10.1007/978-3-319-29604-3_3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2798255$2A5D30C4-D9EC-42A6-8ACB-22DBB84EDC4C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"bb347ea749674b96dcf23d1f480d130c607a21fd","datavalue":{"value":{"entity-type":"item","numeric-id":1791196,"id":"Q1791196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$16B98ED1-D110-40C0-A78D-38A56671549F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3765f4fa456ee10569a1e90d7d16c69c8a5c0861","datavalue":{"value":{"entity-type":"item","numeric-id":2798254,"id":"Q2798254"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$B48A0E65-3490-40E1-BB23-9B74A91B4463","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a2a09b5cba4f9e4657809ce2fd194ee37ff6e885","datavalue":{"value":{"entity-type":"item","numeric-id":2798252,"id":"Q2798252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$932D3128-6003-47D4-BE21-1410C9BA742D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"d632be975d89d9bf6400f8a1a3033c5ac887a3f4","datavalue":{"value":{"time":"+2016-04-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":"Q2798255$3530EAD6-1C52-41F7-B238-2F8A19BF8FBC","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"58b3a5d0bc4bfd215423308dfe52b6887acdeedd","datavalue":{"value":"68V20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2798255$4F163CD7-BCD2-48DA-B6CB-AA810A0BF9D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2798255$441B1B5E-BE9A-4BF5-A8A7-16828676A2DF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2798255$1CDFAE6B-D39E-4CF0-8EFA-6EF514E49303","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"38903aa7c0031396c9bc75c4d3f990381f9f52af","datavalue":{"value":"6562502","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2798255$B0B7FC4A-B4B6-41FF-A00E-EF20CFBEB5F4","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":"Q2798255$C44B522E-0C53-48BB-BE3D-7E3C30D57423","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4dfe52116eea178df8e98fcb66fd7e4802fcbfc","datavalue":{"value":{"entity-type":"item","numeric-id":24263,"id":"Q24263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$308913FC-B804-4E04-81DE-104D83B76A71","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":"Q2798255$43DEF962-7A9A-42C3-B4E3-83CEC5F28911","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"db408f0a5caa3ddf3a1705d552d339d165ab9965","datavalue":{"value":"https://doi.org/10.1007/978-3-319-29604-3_3","type":"string"},"datatype":"url"},"type":"statement","id":"Q2798255$9EC54203-0AAD-4150-89B5-1CF1E70CDE0E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"080a863aceedcd2cdffa3c624a492ec436e12241","datavalue":{"value":"W2403707805","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2798255$828717A7-E5A3-44DE-AF73-6DAE847759EB","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"24730bf218f114d7094d19a6f077dbd4642dc0fa","datavalue":{"value":{"entity-type":"item","numeric-id":5371943,"id":"Q5371943"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$F3ED4B41-8300-4C04-82D8-E84544165039","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c3877a1f64445e2be38ffa92491ece3830dcf80","datavalue":{"value":{"entity-type":"item","numeric-id":916409,"id":"Q916409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$811854A4-DCD8-409D-A74A-8DBA386DF501","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9484c9bc6718b97baddc75a606e56b65c62cc744","datavalue":{"value":{"entity-type":"item","numeric-id":3612622,"id":"Q3612622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$782616AA-0B5C-44F8-8C5C-EFA3FD5F4F87","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03d810ca512b6f14449f91854d88cb7111d9390f","datavalue":{"value":{"entity-type":"item","numeric-id":4370252,"id":"Q4370252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$FAB5BEE1-84C2-4611-84FD-E5EB9E6395D2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dee6886b1b12e58b80eab37b36f8fad3afe11f9e","datavalue":{"value":{"entity-type":"item","numeric-id":2936804,"id":"Q2936804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$CDFB14E7-D646-4E1D-BCA0-1EEEC4C07CAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67b8a6374b4fc895d89506f759c76e54380f8254","datavalue":{"value":{"entity-type":"item","numeric-id":4144755,"id":"Q4144755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$92DC126A-934A-4775-B640-35147DCD4A92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"42767904ec698e77bf5ad5a5ca09192ebfa305eb","datavalue":{"value":{"entity-type":"item","numeric-id":2941173,"id":"Q2941173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$B3DFB6AA-3F5A-4BE0-A89C-4828DE54E07B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6130a72bad290e99b4d30823cf592f64ef05b4a8","datavalue":{"value":{"entity-type":"item","numeric-id":5584402,"id":"Q5584402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$C9344973-3CA4-4FE4-8974-0C904CF3154C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7bb3a3eb73ddc5bb5845397c93ec55eceb2ef8c6","datavalue":{"value":{"entity-type":"item","numeric-id":2575770,"id":"Q2575770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$DB6C2AD6-0E9A-4B6C-9FD4-C6F176BEE3B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c43b86216fe1c5702aab5ae75ac68f23c82c002","datavalue":{"value":{"entity-type":"item","numeric-id":2753682,"id":"Q2753682"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$263B40A5-0BD5-4917-97DC-2862C15BC1EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$3106ACD9-3BC6-4127-9FF5-17D9EE0E754E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8576dc8df0d7857399ab718724b601efc6d9d7d","datavalue":{"value":{"entity-type":"item","numeric-id":3996918,"id":"Q3996918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$D6F9AA29-323F-48C5-9266-41DBB3F591F5","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":"Q2798255$061F6C70-07C1-49B5-A593-2E4E6D974C46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5216594ab26dc420117c0934281b2e8f583a7fe4","datavalue":{"value":{"entity-type":"item","numeric-id":4255591,"id":"Q4255591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$02165CEF-A05E-488C-8BB1-045544B14246","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"211ccd5b5f94c4e816f76718008ebbfd030c7f86","datavalue":{"value":{"entity-type":"item","numeric-id":3183544,"id":"Q3183544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$FB8E751C-AD05-4343-BB70-9861EAAD4566","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"272c5f66ce3cf8d4cd2567af365971d4e849b8d6","datavalue":{"value":{"entity-type":"item","numeric-id":5191092,"id":"Q5191092"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2798255$61845844-46FE-40B5-8147-2EFB2914EA4A","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1dddef22978459d2b01a999c49af777dfeea14e0","datavalue":{"value":{"entity-type":"item","numeric-id":3612622,"id":"Q3612622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8d3bd8da73a8a7c15762ed5396363bb6d9a95ef5","datavalue":{"value":{"amount":"+0.8061843514442444","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":"Q2798255$636D178D-2650-4C36-AC8A-937FB4A830EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46d2f1aea5bca1e9ea33d09f2dc7fd2cfef54aa7","datavalue":{"value":{"entity-type":"item","numeric-id":4790664,"id":"Q4790664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7da22f864127699190f48eb00a2448771c659e6b","datavalue":{"value":{"amount":"+0.7782635688781738","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":"Q2798255$2CDF9821-C27A-4402-BDEE-DC997B3BE80A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"524d090d085cff50384ab46fc0b59b96caa6d641","datavalue":{"value":{"entity-type":"item","numeric-id":3079921,"id":"Q3079921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96a246b7585e7d9a0f973167ec1258af4cff17e0","datavalue":{"value":{"amount":"+0.7597821354866028","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":"Q2798255$C520781D-8D16-4AE4-A29C-77DD4E393793","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c9d9b25e9e0af77fd4831a746fb856aeb5bbfc3","datavalue":{"value":{"entity-type":"item","numeric-id":4037113,"id":"Q4037113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b52e6c8f50763ef0bf36ea5c9f5e958dd0ccba41","datavalue":{"value":{"amount":"+0.7567625045776367","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":"Q2798255$9135E9F9-09B4-4F56-8E42-23653837F541","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc38e2ce3f2eb8018e3b1ff5b6d70c3fd81a9f86","datavalue":{"value":{"entity-type":"item","numeric-id":5712544,"id":"Q5712544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b52e6c8f50763ef0bf36ea5c9f5e958dd0ccba41","datavalue":{"value":{"amount":"+0.7567625045776367","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":"Q2798255$97C90E7B-FE42-450F-9107-C9902CCE34D9","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"From proposition to program. Embedding the refinement calculus in Coq","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/From_proposition_to_program._Embedding_the_refinement_calculus_in_Coq"}}}}}