{"entities":{"Q53719":{"pageid":53775,"ns":120,"title":"Item:Q53719","lastrevid":105429467,"modified":"2026-10-09T10:12:05Z","type":"item","id":"Q53719","labels":{"en":{"language":"en","value":"CRDT"}},"descriptions":{"en":{"language":"en","value":"AFP entry CRDT"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"fe9efebfe020c020554bcc2add330480ca8a839d","datavalue":{"value":"38019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q53719$B912CE26-5A3E-4DFA-BB03-8FA8A31C84F2","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$216D8D34-67D0-4161-A663-59C993330D62","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"8de1c0252bf78dd11914b45975bedccd092a63c3","datavalue":{"value":"https://www.isa-afp.org/entries/CRDT.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q53719$122ADCB8-3CCA-440D-9AD5-FE62861A4250","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q53719$C1401390-275E-4918-AE9B-758C4B2B58E7","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$DE6D2B10-DB68-4E2D-AFA5-42CD13B1C3E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$C359CE8A-52F3-42F3-844F-5D9ECB2ACE43","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e3e9bb7b329ec8e71fcb8b28c9805dd4509dedab","datavalue":{"value":{"entity-type":"item","numeric-id":19731,"id":"Q19731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$3CA51562-380C-42A0-8C19-85DD85E8A72F","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"75cab8c4e7b0beb33bda5c4cedfa0ff28d6e12e4","datavalue":{"value":"https://isa-afp.org/entries/CRDT.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q53719$E7B1BE35-4D07-4DD6-8CB6-1B133BF333C4","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"cebadfd7b78bd04e93befe8d7c5151d4488b7f71","datavalue":{"value":"Victor B. F. Gomes","type":"string"},"datatype":"string"},"type":"statement","id":"Q53719$99C65323-6FED-48F1-9F80-C21D2EA21528","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"4d3b72daa7996cd1fd23c0dd5063ad64b70dfab3","datavalue":{"value":"Martin Kleppmann","type":"string"},"datatype":"string"},"type":"statement","id":"Q53719$3BEEAA6D-8357-489D-A221-79E9A2E9F7E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"ac2a9f431934ff6894f49176eb1b508a5099b086","datavalue":{"value":"Dominic P. Mulligan","type":"string"},"datatype":"string"},"type":"statement","id":"Q53719$5AA32D8B-4FD5-45E0-8A39-2E9D8F94CBCA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"20d545ebbedc0ae2dfdaff93ae5aa814d22aa6d9","datavalue":{"value":"Alastair R. Beresford","type":"string"},"datatype":"string"},"type":"statement","id":"Q53719$8634D335-CC12-4339-86CC-E1C2EAFC4F3D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"523fa94eb2e8565f843706da80ac6263e916b003","datavalue":{"value":"In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter.","type":"string"},"datatype":"string"},"type":"statement","id":"Q53719$30898F8B-E07B-404F-805A-DB52A5F4EFDE","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"bedf9942225faf979656370f4108eb382224db37","datavalue":{"value":{"entity-type":"item","numeric-id":1064056,"id":"Q1064056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$C8F69AB0-140D-4116-967B-E4ACF16BB808","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43cbbc33ad722395bbbcef693c5084530504aa37","datavalue":{"value":{"entity-type":"item","numeric-id":2796275,"id":"Q2796275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$E0CBEEFE-FD03-4D8B-BB7E-CA855B50585A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"547a1aa45f36d0cc467e6694b74c94bd08fff168","datavalue":{"value":{"entity-type":"item","numeric-id":5361944,"id":"Q5361944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$2B50B9DE-5069-4FC9-9A94-B1DB0121E55C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"dc4c5dcb2d36c74238f28ddd1fbfa66787d7bd3c","datavalue":{"value":{"entity-type":"item","numeric-id":5408424,"id":"Q5408424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$0EF9E9D1-3849-4B91-9ED0-C4592A5DC3F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"810ff3068ee57c27f51817524e4d582dc3ea62f7","datavalue":{"value":{"entity-type":"item","numeric-id":3078444,"id":"Q3078444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$AFA2425C-9B22-4B9F-A6EC-E41F82ED01A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"71f014eae90340d070dc667ce0b01474bbb78615","datavalue":{"value":{"entity-type":"item","numeric-id":4371670,"id":"Q4371670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$AADCB0A4-9F89-4727-8258-9FE46A31FAC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e264974062f53b439460b85662778a60b49509d","datavalue":{"value":{"entity-type":"item","numeric-id":2926333,"id":"Q2926333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$3FEAD90C-3AB3-4256-AC4B-6D2AB78D0FBD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fbe1455cc5dda38390654a9baeba09eedb655d2e","datavalue":{"value":{"entity-type":"item","numeric-id":5200015,"id":"Q5200015"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$6FA73668-0689-42D0-AE6E-8A55C8A81235","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bb85590b29131821d96963718430ffa09b000c2","datavalue":{"value":{"entity-type":"item","numeric-id":5408420,"id":"Q5408420"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$A705BADC-AA71-4277-8221-70A3D34709D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1903be4a36187a0a0e197e708bc72f62f93b28bd","datavalue":{"value":{"entity-type":"item","numeric-id":3183520,"id":"Q3183520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$2B1DDBC6-B6F9-49AE-AACC-2E2589C2D236","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"81087b834bd0f0342fd52d99726619dd5c97caec","datavalue":{"value":{"entity-type":"item","numeric-id":3543647,"id":"Q3543647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$B3AE3CEB-83B9-439B-B242-4342056DCAD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d75dbd6831f5997bcd1e3a90202470be0212b0ff","datavalue":{"value":{"entity-type":"item","numeric-id":3638251,"id":"Q3638251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$9B060848-E906-407F-BD00-2C29EEC9E4AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"26f9c9c0da0bc3bdb62c24d5a0777f8a36a55f99","datavalue":{"value":{"entity-type":"item","numeric-id":3766835,"id":"Q3766835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$170E24D6-75EA-461A-8DA7-C18A1D285D8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b79bb6c586431f19bacdd62c3b63263102b465ba","datavalue":{"value":{"entity-type":"item","numeric-id":820129,"id":"Q820129"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$7B966991-A65C-4452-B57B-F2607D28FF5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ed9702c45f558cf37c1cf27f32342d8410b993ac","datavalue":{"value":{"entity-type":"item","numeric-id":4157944,"id":"Q4157944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$CFB5952F-39E9-4212-8FED-8DE681741D9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6db2f02725e1a0df51a2eae8c891243edb57c43c","datavalue":{"value":{"entity-type":"item","numeric-id":5891993,"id":"Q5891993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$DF7DF4F6-98AC-40AD-AFED-7BDD648A72A2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bc1ed2c0c01d7b205a8ffc2309597719b82c231e","datavalue":{"value":{"entity-type":"item","numeric-id":2982319,"id":"Q2982319"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$9516942A-3C61-46F3-B5E2-7DF82014AE9C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2938fa1ea588d049988423b4a7e400b01e9cedc2","datavalue":{"value":{"entity-type":"item","numeric-id":635322,"id":"Q635322"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$CB4D902B-3585-492C-A2A4-9646BA67B50C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8630fbcdc29843e53c7a1293bed413715c1239a5","datavalue":{"value":{"entity-type":"item","numeric-id":1331790,"id":"Q1331790"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$B7E6A97F-9EBD-441D-996C-9E854F785C58","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13b961351448ae339d35d91c7e1441dcfbada5d4","datavalue":{"value":{"entity-type":"item","numeric-id":4904106,"id":"Q4904106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$0C560EAD-23FA-4939-AA6F-84EAB1A1F77A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9435fa2a5e46b6a66fe2cd50eac7a85e1bf9489e","datavalue":{"value":{"entity-type":"item","numeric-id":2829271,"id":"Q2829271"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$9858CA75-EDF3-45C9-B097-BB5255235643","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"998320f8894fa87c8f92dae8b82d30801ffd0cf7","datavalue":{"value":{"time":"+2017-07-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q53719$A7F368D3-6151-4445-95BC-281E40F537BE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"617cb3aa9e16700b87c006045a95f90951fb22f9","datavalue":{"value":{"text":"A framework for establishing Strong Eventual Consistency for Conflict-free Replicated Datatypes","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q53719$0A27C5A4-7C27-48F3-9CDA-D09C3D972F40","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$F7629187-17E5-49FB-BDE6-57619BF8504E","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"c619aaf4eae47fe7f56126dec3ae88d7d608eebc","datavalue":{"value":{"entity-type":"item","numeric-id":7360775,"id":"Q7360775"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q53719$3ED74E1D-ADA8-4D59-8B78-9F740AB037B4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"CRDT","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/CRDT"}}}}}