{"entities":{"Q4916053":{"pageid":6945634,"ns":120,"title":"Item:Q4916053","lastrevid":51697700,"modified":"2026-01-19T13:13:43Z","type":"item","id":"Q4916053","labels":{"en":{"language":"en","value":"Producing certified functional code from inductive specifications"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6155869"}},"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":"Q4916053$A72972AC-2A4B-4E48-B819-0B39D5C8262D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4a90c17110296067d790b370f418f161d3979ff8","datavalue":{"value":{"text":"Producing Certified Functional Code from Inductive Specifications","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4916053$2E8009C3-4776-456E-B03B-481538217825","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"b811fc61592c826060fda335a2027bf084fb2972","datavalue":{"value":"1383.68018","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916053$AB9912C8-5494-464D-9BD9-98DCE8EC3E18","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9988ecee7c019463f219dba5bc619f64c3611c7d","datavalue":{"value":"10.1007/978-3-642-35308-6_9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916053$A7266C2F-038E-4167-9009-8318949DA8CC","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3eabb4fe6ea224dcb87a1e33cfd302c8dadfe977","datavalue":{"value":{"entity-type":"item","numeric-id":4916052,"id":"Q4916052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916053$2237A2A3-2D2D-4213-B212-392DC76E1D86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"786f6c8f2a36da61e98b228bbd36b74e25ad6f92","datavalue":{"value":{"entity-type":"item","numeric-id":2104524,"id":"Q2104524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916053$DAF62E26-3E17-456E-83B8-79976FDAD502","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"f8c40e2cd3207dd1d19085f0b79e8fee7be86ced","datavalue":{"value":{"entity-type":"item","numeric-id":1624591,"id":"Q1624591"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916053$50F934FF-D97B-479A-8F53-D72B81E09CE6","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"19e7468504fbcb9c3a09d3a38cdd67d03e02eec6","datavalue":{"value":{"entity-type":"item","numeric-id":2938035,"id":"Q2938035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916053$16F43834-46AD-44B2-825B-F4A2D4DEAA6F","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"09328fefd4bef3fd48b14da7de769686b3303861","datavalue":{"value":{"time":"+2013-04-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4916053$ED577FDC-4BEE-40D2-B962-73BD37A8320E","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"136db5bb8708e52501dec32644ab90fd42c4c538","datavalue":{"value":"68N18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916053$BF3F0977-3F9B-4F24-8EF3-72952BB224E0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916053$298CD056-4E9C-4A53-992B-9B8172074ECE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"3dc2508f2596f251c26abf89e508b25af72384de","datavalue":{"value":"6155869","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916053$24C9DCF8-64FE-4A74-A05F-5AC47FB61858","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f75653c44e6bce51d80c3c3a8ae08ee14a231fcb","datavalue":{"value":"executable specifications","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916053$1C93096B-6FC7-4592-99B0-E6B5D18CF995","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4e15125f85588f39fa5297c96b5b7219fe35abdf","datavalue":{"value":"inductive relations","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916053$F073C956-1926-4A52-A58C-A272F0E8FC2B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"04f2c0e3bec5cbd36b73a8ef58aef7e0d258497f","datavalue":{"value":"functional code generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916053$52D6F526-8895-4A96-8A84-132A93C9C9A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"735ca379ec5602cde56b6fbdf54cd51085e7220d","datavalue":{"value":"soundness proof generation","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916053$C88E600C-612E-4AEE-8827-DA669F1BF2C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q4916053$0B96B60C-070A-48E8-8BAD-0A08A44076AC","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":"Q4916053$73DA7DC2-2160-4BC5-B70D-C18C4EF41AA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040fe209bf9959da562393c0e37eb31592733af3","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4916053$C4D22C58-8AC3-49B3-B3F5-1BD2629ED84E","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":"Q4916053$F77334C2-4C0C-4F3B-B688-11AA6AB722F5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a8ebfb9ffba32a080a4e37ac8b6398ef4705e361","datavalue":{"value":"https://doi.org/10.1007/978-3-642-35308-6_9","type":"string"},"datatype":"url"},"type":"statement","id":"Q4916053$04572CDA-D405-44BE-A589-D47ACA53EAE1","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"da7114c58181b8b2feb5569fdbf7950b83144702","datavalue":{"value":"W126590973","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4916053$CC27DF4E-1E7E-4DC2-8264-4879F1B5DFE4","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":"edaba969eb960ac45eb447ac7530fd4071ffe5c3","datavalue":{"value":{"amount":"+0.7761583924293518","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":"Q4916053$630E1493-AF0C-42E2-B9FD-64F6FC77C061","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":"08dec4fdca07f3e047b5a9367203a17703e89ee6","datavalue":{"value":{"amount":"+0.7712916731834412","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":"Q4916053$1C5C3B97-E27A-40F1-90DD-70EFF8603A0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"36d82340558da6eb9a0aa771f2d14217a2a14c70","datavalue":{"value":{"entity-type":"item","numeric-id":3523167,"id":"Q3523167"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e9d9c0ecc54e8cdb7b1c755543ff06d051315a39","datavalue":{"value":{"amount":"+0.7556032538414001","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":"Q4916053$23C469D3-5DCB-4B82-9CF2-F26175F7EACE","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":"fd12abedfab85d1733f01ade9e1304f5867c8a45","datavalue":{"value":{"amount":"+0.7472095489501953","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":"Q4916053$783947EA-FF5F-4797-9BDE-481D7640ACE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f959c7712c196883e995861185c429abdff17384","datavalue":{"value":{"entity-type":"item","numeric-id":4944851,"id":"Q4944851"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f3ae9a853076eec25d3e9eecc8d1c098ad103414","datavalue":{"value":{"amount":"+0.7472090721130371","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":"Q4916053$AE4DF11A-4D70-4286-9AD7-F63168E0C61C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4916053","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4916053"}}}}}