{"entities":{"Q4917993":{"pageid":6947575,"ns":120,"title":"Item:Q4917993","lastrevid":51708338,"modified":"2026-01-19T14:53:40Z","type":"item","id":"Q4917993","labels":{"en":{"language":"en","value":"Formalizing type operations using the ``image'' type constructor"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6160409"}},"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":"Q4917993$9D35497E-F694-4375-A855-73348044B0AB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"9dd3365e445e0ba5436f9820cae33a32969d3d72","datavalue":{"value":{"text":"Formalizing Type Operations Using the \u201cImage\u201d Type Constructor","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4917993$D6937103-21AB-49B9-9DA6-4410B94B0424","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6c67b58c5b80280dad5b9929b614a17fe28f164c","datavalue":{"value":"1262.03025","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4917993$7D91AC37-DE97-45CE-9B04-67B443B4E296","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$5D51E4BF-34C0-4460-8147-FAF2206180C0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"f67cff4992b4af716700e591fa06388150841fb3","datavalue":{"value":{"time":"+2013-05-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4917993$462A3443-A609-4F17-B130-551AF3CAAE47","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4917993$0F4D49B9-A52D-4239-AEBD-DBE94D3E76FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4917993$B087759B-B7FD-48E5-A3A4-CCBABD1B7CF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4917993$01963E02-C91E-4451-8C68-2311E560819F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"47cdf585d6ffa4620f0c54b75f5e7b2f39a181f1","datavalue":{"value":"6160409","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4917993$AE6E2BC5-AE21-499B-AB26-A08E004B410C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4917993$E378F0DD-8FF7-476C-8DFC-38523F87DD86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69eaa0b39db33bdfb90e0e2fdc84d350c2fd3843","datavalue":{"value":"type constructor","type":"string"},"datatype":"string"},"type":"statement","id":"Q4917993$0E028367-92A5-4762-91B9-E28C6FCDA00F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4016738090a05d55b312502aeb38cefef3e9129a","datavalue":{"value":"\\texttt{NuPRL}","type":"string"},"datatype":"string"},"type":"statement","id":"Q4917993$BF24ED0B-D6CC-4E76-8A29-2FA12A1B4A6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"acdfa1f5b5440a9cd983f47cd7d02a25daacb7b3","datavalue":{"value":"\\texttt{MetaPRL}","type":"string"},"datatype":"string"},"type":"statement","id":"Q4917993$A7FA5E58-D06B-4188-B235-F523860C4E35","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"905c185b35495bc6c5c2ada6dd808940c7264ec2","datavalue":{"value":"\\texttt{Coq}","type":"string"},"datatype":"string"},"type":"statement","id":"Q4917993$BBDA1B23-9D3B-46E1-8F28-88ECD4058145","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"aacdd9e6b1e081b5de4688ca768accb91a2c66bc","datavalue":{"value":"calculus of constructions","type":"string"},"datatype":"string"},"type":"statement","id":"Q4917993$74256498-14FD-4D9E-8260-1D0F56723E25","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fef5f048f2ff970244195639e7bcf4e64ea5e666","datavalue":{"value":{"entity-type":"item","numeric-id":16795,"id":"Q16795"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$218C6FBA-E24A-49DD-B796-76E8CA7858D9","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":"Q4917993$6AB4C5EC-5223-4D81-B507-A79EFFB7428E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"27b6ae20da44d6f09b655d9481cc0df08a8ffcdf","datavalue":{"value":{"entity-type":"item","numeric-id":18826,"id":"Q18826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$AD1BC975-FDAF-455A-8D33-B3F6E618961C","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":"Q4917993$AEB949B9-1A5B-45F1-B6BE-A8C40AFFCEBC","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"398fcfadc5c501d69cf06fc09b3df5b56d5a5c6f","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2006.05.041","type":"string"},"datatype":"url"},"type":"statement","id":"Q4917993$4FB43EEA-CE6C-4BDF-B4A9-AAE1397EDF59","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"0843d40103db0f78f4574b9f473414fdc4a47eed","datavalue":{"value":"W2096220787","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4917993$67CC0FDD-A0B7-4E10-B4E0-B9DDF6F08382","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8f87d8e5bd977e16361b925f06b414543ca3a38a","datavalue":{"value":{"entity-type":"item","numeric-id":3823124,"id":"Q3823124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$83FE664A-7E8A-4D9D-969B-BFD3BDE97BDE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7931dc29f3e5a2a167917b66423fa0388ae2206f","datavalue":{"value":{"entity-type":"item","numeric-id":911744,"id":"Q911744"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$387F2179-CA30-41DF-80F7-90D2513F9B3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"833dcd364e57e6d19a2badb86e03ce65aa5821b7","datavalue":{"value":{"entity-type":"item","numeric-id":701699,"id":"Q701699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$A2C40A19-E758-4C77-BE70-03F557268B17","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":"Q4917993$98F5C81A-EB4D-4196-916F-53500E1D0264","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"95495a8e4f0058056e049e538f11019cff0c80a0","datavalue":{"value":{"entity-type":"item","numeric-id":1416071,"id":"Q1416071"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$ABBE8EA0-77FD-4F5E-BACE-EB8EE1644EF8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"978af8987770da9ce87981964976dc7a47a0da09","datavalue":{"value":{"entity-type":"item","numeric-id":3204055,"id":"Q3204055"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$899F66A0-C43E-4C49-A3B8-B33E236CB125","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b0ec3118c55b6f3ab232f29debefc8c9d383a9","datavalue":{"value":{"entity-type":"item","numeric-id":3688389,"id":"Q3688389"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$0653DA0B-8434-4452-B619-FE7A5F55B690","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8a5184581920ff2bf9fbe1aa78428d2a44a27c0","datavalue":{"value":{"entity-type":"item","numeric-id":4484345,"id":"Q4484345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$D3745558-483A-4F89-8094-84A5745C30ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea5789bc155ab0b987340c5a4699fc00916ecad4","datavalue":{"value":{"entity-type":"item","numeric-id":4484346,"id":"Q4484346"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$DAE81AAB-4D59-49A8-8AA9-095002BD88B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"384c88ee747368e498e55b1ebc22017816448ffc","datavalue":{"value":{"entity-type":"item","numeric-id":2265415,"id":"Q2265415"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4917993$DC479175-F96D-4241-A29E-2C4FEF674609","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"18ef66df495395ad1fada596909211a93102b8f4","datavalue":{"value":"10.1016/J.ENTCS.2006.05.041","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4917993$1719E8CC-3610-46C1-B814-9F29E7649813","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f7e4383c2ecd4e64a678e674cd670b84f21f373f","datavalue":{"value":{"entity-type":"item","numeric-id":4484345,"id":"Q4484345"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2418d1718488129b3e475ad035fba6f2e5032a4f","datavalue":{"value":{"amount":"+0.6957840919494629","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":"Q4917993$45968BC7-B1AC-46B1-BE69-CBB89B68668D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"46d5eb500b91b900b7e0ec167e7c875fd9ecd2d8","datavalue":{"value":{"entity-type":"item","numeric-id":2828239,"id":"Q2828239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9e46c640b5292e24e23801f9e573886a4ce8428c","datavalue":{"value":{"amount":"+0.6947588920593262","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":"Q4917993$F8C1F267-D532-4E24-AE43-611E700A326B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f6d9ad8a5278ff1762ab5c08f1e1ae920ab20436","datavalue":{"value":{"entity-type":"item","numeric-id":1199709,"id":"Q1199709"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6405ac4f261d2de7034f2e909bf1edfc6a126032","datavalue":{"value":{"amount":"+0.6638442277908325","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":"Q4917993$9439531A-0C79-47CC-84BA-C14EE92BB29C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"72b22966b1a2704c315082d7608da491f0c28146","datavalue":{"value":{"entity-type":"item","numeric-id":4945203,"id":"Q4945203"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"270271aa1e79fe8c60acc03cfa15d930b750e39a","datavalue":{"value":{"amount":"+0.6589679718017578","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":"Q4917993$B7B09FC3-685E-4E27-8A8F-6B1A7D6F4A48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"aa98d1622017fdb4d9d5836da95a192f53f9e4b4","datavalue":{"value":{"entity-type":"item","numeric-id":4883281,"id":"Q4883281"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b102c9d36a1c4c2f7b79e14ff3e6ccfbcebd329b","datavalue":{"value":{"amount":"+0.655354380607605","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":"Q4917993$304A988B-6C99-4304-8F07-EA0705F1F3C2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4917993","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4917993"}}}}}