{"entities":{"Q3058448":{"pageid":3069164,"ns":120,"title":"Item:Q3058448","lastrevid":51134612,"modified":"2026-01-16T20:55:02Z","type":"item","id":"Q3058448","labels":{"en":{"language":"en","value":"Programming inductive proofs. A new approach based on contextual types"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5818172"}},"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":"Q3058448$78278E60-4A44-463E-B57D-619B8CB41C8A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"29254617e8335dcaa1507f9cc6eb43d0ca1f472e","datavalue":{"value":{"text":"Programming Inductive Proofs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3058448$AEEA4994-0108-45D3-9AC3-A6F8743061B6","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"22d1fac7cbdbfa7067ec9ba900f3843194b3c7fe","datavalue":{"value":"1309.68051","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3058448$E6B0C980-49A9-4B7D-9B09-5D5966F026C6","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"730dc439850f303088179acad0f54dd5f01c37f8","datavalue":{"value":"10.1007/978-3-642-17172-7_1","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3058448$55AA510D-163F-4E86-84E3-776784D202BF","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":"Q3058448$36DF8D92-80F1-439E-97A8-76294BE0D421","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"45799abc9832f373d48a10466fe1bfbd3b97c8b8","datavalue":{"value":{"entity-type":"item","numeric-id":3058447,"id":"Q3058447"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$D44FE3DE-F3B5-4B5C-A60F-4BA075570CCC","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0597dd9f38cc744686ebfdde0ab7e717b4afd491","datavalue":{"value":{"time":"+2010-11-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3058448$69CCA982-37D5-49AF-A024-5A4E8876BA04","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3058448$2122386F-81E6-46CB-BB93-6ABCBED84D93","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3058448$BBBA753E-A5CF-4F54-94CA-80A39D2AE750","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"54e482e771e6f938c12d57c5d391cdf8646683be","datavalue":{"value":"5818172","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3058448$609A63CF-75E2-4E0F-8FC9-5472ACA87FFA","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":"Q3058448$CC6608A8-C5F3-4216-B18C-782B4742DDAD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"86fd017762a2cc84520acf70ff19531594c257aa","datavalue":{"value":{"entity-type":"item","numeric-id":33173,"id":"Q33173"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$75089736-95E1-48A7-81D4-08FCB9B3173B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8be5ee5254d2a781e0ec7bc0b35265c3f1813a9a","datavalue":{"value":{"entity-type":"item","numeric-id":22078,"id":"Q22078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$AC58618A-8AF8-42DE-904F-D271DD7B8CA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"666b9a47dc68ef552d799234146196fb61f3c743","datavalue":{"value":{"entity-type":"item","numeric-id":33169,"id":"Q33169"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$32A92E9F-BAA5-44DF-B1EE-2D7DE3E4CA35","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":"Q3058448$5E414D49-1C06-44C0-99CB-DF1E05B3A053","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":"Q3058448$C037EB80-E173-4E73-B2A1-3D79B2A5B92F","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":"Q3058448$13719B36-D037-4D5D-B15F-C294A449F3F3","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8a723cf3daf8f54844e7b01b9d3f6dc93a824893","datavalue":{"value":"https://doi.org/10.1007/978-3-642-17172-7_1","type":"string"},"datatype":"url"},"type":"statement","id":"Q3058448$0AA0C8BF-6CD6-4A74-850D-0E1BBF9A63A4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"329ffe1f5b9e9e9b283def94eeadb49968c10f1b","datavalue":{"value":"W197201650","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3058448$DB1F88C3-A126-4528-A8BC-4111A1ECD123","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"79ce8544fc5a0489695eae9a558cb4d34b573281","datavalue":{"value":{"entity-type":"item","numeric-id":5477646,"id":"Q5477646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$3195388A-3AAB-4DFE-AE06-3D9C6379BDE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5249c80fcd11fa0612fb7dd29644b8dc29907a14","datavalue":{"value":{"entity-type":"item","numeric-id":4939690,"id":"Q4939690"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$4F9EA943-CCD2-4DBE-A603-C43AADD5637E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d8bfe191ca90d3395347096033dd0a0643030e0","datavalue":{"value":{"entity-type":"item","numeric-id":4281462,"id":"Q4281462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$03B7ACD9-C21F-48EB-9BBB-6424F2C67883","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0d16ee5e65f1db51f9c436dbb90be9daf0b8247a","datavalue":{"value":{"entity-type":"item","numeric-id":5255065,"id":"Q5255065"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$52A40E55-D306-41B0-8D25-1684D10F10CF","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":"Q3058448$6617DEAA-1EAF-4098-8DE9-B136D9D85ADE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bbda4d5d2fa3599cf321b083730ba47f18179a2","datavalue":{"value":{"entity-type":"item","numeric-id":3024905,"id":"Q3024905"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$A8346E73-CD6C-4087-AD2B-7DA81D4AF9FC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2dd90ba3b3c5e17240dddef25d5b236eea01d9de","datavalue":{"value":{"entity-type":"item","numeric-id":5747652,"id":"Q5747652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$D91DD963-FA9C-45E2-98F7-51748E6E05EB","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":"Q3058448$5D20723C-252D-4C1E-9488-D96E9A4AEB8C","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":"Q3058448$0031656A-9037-4296-9F42-FB8CA2DEEEF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6063e4a144bafe1447ae8b10555347d26c418f1d","datavalue":{"value":{"entity-type":"item","numeric-id":3189797,"id":"Q3189797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$8902E504-CEBA-4475-8623-6C23B79F7A1E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"333782dfe2a782886768e8c7561d4e8bfd035e1a","datavalue":{"value":{"entity-type":"item","numeric-id":2655327,"id":"Q2655327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$3E90AB60-FD77-4BBD-9A90-072C69380152","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":"Q3058448$E904713E-2C3B-423D-BEFE-4D17424B348E","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":"Q3058448$D6CF11D5-C238-42FE-B4CB-6741FC1CEAB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5333f404cb1c5a483ee97a9aa8db2143fb09170b","datavalue":{"value":{"entity-type":"item","numeric-id":4012879,"id":"Q4012879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$BB346233-D194-4684-851B-76ADDC5E71B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"441ab522372dbc56337549e9359e4e2646de59a9","datavalue":{"value":{"entity-type":"item","numeric-id":850496,"id":"Q850496"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$B2BCFAC5-937A-47B6-BB40-29DF4B3AE7A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b6db6d308bb0736931a5316de4b01d030f7fbed4","datavalue":{"value":{"entity-type":"item","numeric-id":3523179,"id":"Q3523179"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3058448$26FBB5FD-A7C2-4206-9881-38690579CF19","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":"Q3058448$825E621A-F557-4949-8FEA-22AC9FD2C5A1","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":"a759c0f756f3a39987e42fbb5ca952dd2a7717fb","datavalue":{"value":{"amount":"+0.8657562136650085","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":"Q3058448$18985EA4-A0A3-477E-843F-9FCC09665C23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d4b130ba3f3ab353eb95092c98b979c20e43019","datavalue":{"value":{"entity-type":"item","numeric-id":3454100,"id":"Q3454100"},"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":"Q3058448$7BE3D4F4-1FE8-4694-95B5-812CED7EA66F","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":"fc9c8683b21e48d5d6b8433ad445b7a61f7cff39","datavalue":{"value":{"amount":"+0.7575639486312866","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":"Q3058448$69D17F27-070B-431F-B42C-104EB8721ABC","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":"a7976a6a166df472fda51f9d58b22f5a9f7e9d59","datavalue":{"value":{"amount":"+0.746121883392334","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":"Q3058448$C8EF2F67-2ABE-4D33-802B-D11427A7FAF2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c823eb76233e4855e66828e769991a47beaee71b","datavalue":{"value":{"entity-type":"item","numeric-id":1190474,"id":"Q1190474"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"150e216cf224c4d6afab314dddd0286258f0eaee","datavalue":{"value":{"amount":"+0.7459612488746643","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":"Q3058448$BFC3F875-98B9-454A-8C9D-FF9CCB6A906B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3058448","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3058448"}}}}}