{"entities":{"Q5081874":{"pageid":7111450,"ns":120,"title":"Item:Q5081874","lastrevid":55412869,"modified":"2026-02-17T15:50:15Z","type":"item","id":"Q5081874","labels":{"en":{"language":"en","value":"The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7543890"}},"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":"Q5081874$2850E0E4-A3E5-45EF-A255-6A9EC0000CA6","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d5343a56ef810032eb299d762d9435c4b810c29b","datavalue":{"value":{"text":"The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5081874$DF425DCB-046A-4556-B281-C67DCFED4DA7","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b1bd78b6f2af61fd65b7e8a8f7d7802f21e39216","datavalue":{"value":"10.1142/9789811236488_0008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5081874$1C26BF8A-0459-40C4-AD43-92E09A6B01B9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fa467ab0fb5921a8aef55b984db7a2882bc4957f","datavalue":{"value":{"entity-type":"item","numeric-id":877885,"id":"Q877885"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5081874$B424546A-2AAB-4886-84B0-D11C55486C2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"ef4a01f54f3e349b8ab6cf4271ef92b1d9a9ead8","datavalue":{"value":{"entity-type":"item","numeric-id":1395675,"id":"Q1395675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5081874$45EC19FE-0369-4C54-BE6A-555CF68C2F39","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"eb6635041af2fed8b191d71905ffc43da2af873e","datavalue":{"value":{"entity-type":"item","numeric-id":5081865,"id":"Q5081865"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5081874$FF058F8B-A18E-47F0-AA31-E1EE65219170","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"eb05ecdd4c1bc9bc017712b48f5ce5d7c83890d5","datavalue":{"value":{"time":"+2022-06-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5081874$E1A87F17-C421-4556-B166-F5C54C708597","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"d0122a76a4da73ddb0e974bb0b62c90364029340","datavalue":{"value":"https://hal.inria.fr/hal-03338785/file/the_braga_method.pdf","type":"string"},"datatype":"url"},"type":"statement","id":"Q5081874$E7396797-ADE3-4858-BD04-ECB0F6ACD13C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7a1d4d343889492e30dd853837039fd3cd08322a","datavalue":{"value":"03-XX","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5081874$FD65D048-BBB5-44AD-8E2C-020D117C82E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"56528a547afad658a2bccf50696c0882526c82f7","datavalue":{"value":"03Dxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5081874$2E131AEC-6554-455D-942B-B6BD0EDE875D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a16b2d00f5f309ca4243bc382dd94889099a0bfa","datavalue":{"value":"03Fxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5081874$4361033F-0F42-45D7-935C-39ACB71F8408","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"11cabf296cbf78cefb4c4e9ef3c9625682c34a7d","datavalue":{"value":"03Bxx","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5081874$8FB97F32-278A-412A-85CD-4AB8CB35D178","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a6e1d5311aa888845abd7ed04083527502f1abbf","datavalue":{"value":"7543890","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5081874$0616CD26-7FCE-44A9-8B40-540E34E6427C","rank":"normal"}],"P1463":[{"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":"Q5081874$074733F4-B260-47AA-B480-5530EF763ABF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"4feaea7961d9cfdcd7e2968b41cc11ecb0c87f44","datavalue":{"value":{"entity-type":"item","numeric-id":21716,"id":"Q21716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5081874$7E526CC7-7766-43E8-9DFF-69AD45D623A4","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":"Q5081874$1DB162D2-DEB5-4505-ABE8-374DF8804D76","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":"Q5081874$367EBF4B-D61C-4DA8-A3C3-11D43EEB2B5E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f24c20f9a96752bd7f2be09d3b4f10ba27632dea","datavalue":{"value":"W3188171585","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5081874$7FF45132-7017-483F-A0B5-C414433A77E5","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"126be7296d6b7110e1000144e41a4b9d8fcc6ece","datavalue":{"value":{"entity-type":"item","numeric-id":4435471,"id":"Q4435471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"720b5ad3c71f7a682318255f3bbc9c456bddcc38","datavalue":{"value":{"amount":"+0.7418379783630371","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":"Q5081874$D9E37902-551F-45A5-B039-EFDD5B29DFB7","rank":"normal"},{"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":"e07c3f2dd308cc5988764a266340b76030acf44b","datavalue":{"value":{"amount":"+0.7395812273025513","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":"Q5081874$90B9CB1B-3110-4925-B79B-7435D27A421E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e87c2ec4d598babe4de07916468d590933627ef3","datavalue":{"value":{"entity-type":"item","numeric-id":6083698,"id":"Q6083698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"88104d6106b3d102fbdc66b861a46ed4a28ff221","datavalue":{"value":{"amount":"+0.7147248387336731","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":"Q5081874$F2972C52-B61B-4103-AC3C-061141E7AF6E","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":"cff0ebbb2dfd7ed8cc731202edd5c00eafe1db6e","datavalue":{"value":{"amount":"+0.7145600318908691","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":"Q5081874$886B4F6A-24A8-4397-8558-B20C32454451","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"622d51dc706493176237d6f56355331d44c81130","datavalue":{"value":{"entity-type":"item","numeric-id":2743705,"id":"Q2743705"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e501a2b6eb327c2d4db381f08c50129d58ed023b","datavalue":{"value":{"amount":"+0.7111144065856934","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":"Q5081874$72A69738-0AD3-41CE-AA1A-9440DF0F500A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5081874","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5081874"}}}}}