{"entities":{"Q3454100":{"pageid":5233500,"ns":120,"title":"Item:Q3454100","lastrevid":52405952,"modified":"2026-01-22T14:06:11Z","type":"item","id":"Q3454100","labels":{"en":{"language":"en","value":"Inductive beluga: programming proofs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6515512"}},"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":"Q3454100$E0227F41-9E53-4F08-8148-C5A957218319","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"e991cf67e9e36b0ac58b8c9e3bd92212a2c1200e","datavalue":{"value":{"text":"Inductive Beluga: Programming Proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3454100$37A6881D-ABA2-4941-8887-82F79A301B90","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"bd5f32643a36e51edb242e3d39846ef705b77e60","datavalue":{"value":"1465.68294","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454100$1229C284-89B9-4936-A5E7-390070229328","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"8ead7cdcf966b4d54318dfa742687acc85aa5114","datavalue":{"value":"10.1007/978-3-319-21401-6_18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454100$7B7470E6-13E5-4477-A21F-5E1A7A78B883","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"8825a5f48e59e5b1e1510e59d52fce48da47c37b","datavalue":{"value":{"entity-type":"item","numeric-id":229739,"id":"Q229739"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$2A7D7B8F-6784-40A2-BBA4-B72C444DF49E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"15cb7e723c6ba3637d8c83366f88049fd361bce2","datavalue":{"value":{"entity-type":"item","numeric-id":2942889,"id":"Q2942889"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$45DA396D-6E2A-4BA8-A862-21926FFD3D05","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3cc4c7edeb37e5e3024aeff0de74501df6e066e3","datavalue":{"value":{"entity-type":"item","numeric-id":3454078,"id":"Q3454078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$2B06E9E2-148C-495A-9284-F8F55E9E3EBE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"9f34c33daac76be2878f4eb0eeca7aa927e679a8","datavalue":{"value":{"time":"+2015-12-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3454100$59285242-627D-4D0B-816B-644FCD8A8342","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454100$6D738EFC-01C7-441E-9C85-4E58971CB347","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454100$DF8AAA4C-B3C3-42A0-B8B8-4C52E8AF6426","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"806544a60c0620fa11eac3f09d64e16fd780e238","datavalue":{"value":"6515512","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454100$0C7BFE00-3797-4B30-AF2A-8E1A9F2C3ECB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66040eec798fa7d182443c16b59531175d83cf5e","datavalue":{"value":"logical frameworks","type":"string"},"datatype":"string"},"type":"statement","id":"Q3454100$99AE8788-5D24-4D89-B3AA-9917DF7107ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e22447b229c7a32c8d247e1ea4002861fd0fbd68","datavalue":{"value":"dependent types","type":"string"},"datatype":"string"},"type":"statement","id":"Q3454100$FE7962E7-91B3-407D-B903-82C4564F1634","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q3454100$E48A3258-C6E9-4ABA-93FC-41732025894F","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a8e56b54ce67b3f3451fae93e0a157bd7197fba1","datavalue":{"value":{"entity-type":"item","numeric-id":21444,"id":"Q21444"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$2F02253B-FEC0-4B9D-B2FE-7FBC342F2690","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":"Q3454100$03FAAE78-5706-4131-B12E-FE821FF88E24","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"05e19126d9e9907924a4600d0a5598afdc2c5f70","datavalue":{"value":{"entity-type":"item","numeric-id":20609,"id":"Q20609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$5B19CFDE-9B7D-4F46-B966-0FA5F49B0F30","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"be9a1fdbfd35f7a816de32e6d9d9a2a21796c942","datavalue":{"value":{"entity-type":"item","numeric-id":14061,"id":"Q14061"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$48127EA4-FB5B-4552-BB98-56A6F926F284","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":"Q3454100$1E9EB8E9-B94F-4AE3-9688-51B38EBCE1EB","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"2f7bc2425faa70bf4c790f689f1dbdeb7b57eb51","datavalue":{"value":"https://doi.org/10.1007/978-3-319-21401-6_18","type":"string"},"datatype":"url"},"type":"statement","id":"Q3454100$B981AD13-FC5F-4C5B-9DA5-39B69E067139","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e5721eaada32aa33cdc59752877585b73fe297a7","datavalue":{"value":"W1433844459","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3454100$0B85EDB9-B428-4D73-BA44-73ACA5A2CA40","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"88745a0cd3171e11c93f43d8028df53fdd6dbc87","datavalue":{"value":{"entity-type":"item","numeric-id":2938052,"id":"Q2938052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$E26DE00D-AB0E-46AA-A4A1-8B9D81F0EB08","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$C7A11373-0529-47D7-B406-3025D2959733","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"228e40236d38aec5a149d907ee03718626a60ccb","datavalue":{"value":{"entity-type":"item","numeric-id":2942890,"id":"Q2942890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$5A6C427C-3EFF-4C1F-89F9-8188A8807010","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b3dac70721402a09d65f93017a3ee67f0fd9d1c8","datavalue":{"value":{"entity-type":"item","numeric-id":2804942,"id":"Q2804942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$DB6F3814-AE04-4CEB-8A26-1874F1A42F4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cf284620825356e4026f7163726a6eaa28789317","datavalue":{"value":{"entity-type":"item","numeric-id":287277,"id":"Q287277"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$BCDB77EF-88EC-4DBF-927F-1F8C1EBDA4E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ebd2134f394c79633368977edccb4641841638f","datavalue":{"value":{"entity-type":"item","numeric-id":3541698,"id":"Q3541698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$2B874524-8B9F-4D78-860F-45D93BB45F62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$641F19EB-B5C9-412F-8C30-524DA8AA7A9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84bb99210fcc9b5282870c32fda47e82c20e574e","datavalue":{"value":{"entity-type":"item","numeric-id":6083695,"id":"Q6083695"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$9EE781C8-FE15-4AEB-82E5-15DBBCFD4071","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"45d621c08d6b6b648b2f02de3b6f7c65499ed1c5","datavalue":{"value":{"entity-type":"item","numeric-id":5277812,"id":"Q5277812"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$FAD80156-8364-44EA-9A5A-CBDA783B79D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"88dd97334618a8abcb30d6b953aa7791488fcf62","datavalue":{"value":{"entity-type":"item","numeric-id":3189856,"id":"Q3189856"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$8BE3F294-7DAF-41C2-8BAE-027F9FDDDD2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6b19eae06ce0ec3719d39a65466af8f728d39032","datavalue":{"value":{"entity-type":"item","numeric-id":4912883,"id":"Q4912883"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$BA25EBFF-4B27-48AF-A2BE-DC62CC62D978","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db64b11464b9db48e2a389bd15fbba45af72595f","datavalue":{"value":{"entity-type":"item","numeric-id":5277845,"id":"Q5277845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$09026851-1F92-4010-A788-9B8986339813","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a90a510f27550100d45a2ef21dd83bca5c9e1966","datavalue":{"value":{"entity-type":"item","numeric-id":5747747,"id":"Q5747747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$E08EC668-5F28-4597-8BAC-7DE9B6E9ACA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c7130b8e8ad403bac4e3a609004e5598d1175d3","datavalue":{"value":{"entity-type":"item","numeric-id":5561939,"id":"Q5561939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3454100$C978B56A-884D-43DF-BA9B-A658B04A7FB9","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3d9d546752157f9e756c98b4a253aee9c63c89ab","datavalue":{"value":{"entity-type":"item","numeric-id":5747747,"id":"Q5747747"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a2549700235c088920ed28414490a83a7d0c2a8","datavalue":{"value":{"amount":"+0.8648804426193237","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":"Q3454100$B9CB8D63-5E8B-422A-9AD1-6F74AE1E8861","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7609494392bb4215d21f7a8a3e5f08d86684fe14","datavalue":{"value":{"entity-type":"item","numeric-id":3058448,"id":"Q3058448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e5f006a0efaed875b869d3e7b90b761e417f8a78","datavalue":{"value":{"amount":"+0.8647204637527466","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":"Q3454100$912E5E23-DFB8-4702-BC9E-4CB263E15EC3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"058758f3ede8cf6908f9bf9e85cb8f830d733728","datavalue":{"value":{"entity-type":"item","numeric-id":4691187,"id":"Q4691187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a2161b5be749861b804a962a7e3d2d28686384f","datavalue":{"value":{"amount":"+0.8507842421531677","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":"Q3454100$1C4524A0-B74B-4ACD-BA7F-1DAEA030646A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38aa120b25c6a2afd536e54ca4c3bec74fcc152a","datavalue":{"value":{"entity-type":"item","numeric-id":5236557,"id":"Q5236557"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0621b53bb2edd32dd4196678ba08f6a60e99e50e","datavalue":{"value":{"amount":"+0.7797847390174866","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":"Q3454100$10BB8E7B-1D55-4768-B13A-98B976D9B7A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e3a108876ee2d73cf53e48814576175e292747f","datavalue":{"value":{"entity-type":"item","numeric-id":5110924,"id":"Q5110924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d2b5b17a22362464c1d288643536fd677694f41f","datavalue":{"value":{"amount":"+0.7603596448898315","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":"Q3454100$8F4C7397-315C-4C43-AE9C-C6673BC5FC8B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3454100","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3454100"}}}}}