{"entities":{"Q4647575":{"pageid":6677156,"ns":120,"title":"Item:Q4647575","lastrevid":53321222,"modified":"2026-01-24T17:45:06Z","type":"item","id":"Q4647575","labels":{"en":{"language":"en","value":"Internal type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7002049"}},"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":"Q4647575$8DBAEE3A-5215-4031-8B04-071119AF50FC","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8c73d4d41bb5b7005d8e0ee271586e4d02d714e7","datavalue":{"value":{"text":"Internal type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4647575$D8EB535D-7288-47BD-9F66-28A87E1B3571","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"4bc3a01f12d2d73c58c136a81d38e26fa0ff8f55","datavalue":{"value":"1434.03149","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647575$859C50F8-9F8E-4836-92D9-522368AC2FBA","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"cc4375c9fad2fc840a7c870e3d6b4cb807084506","datavalue":{"value":"10.1007/3-540-61780-9_66","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647575$C39F6D79-6FDF-48DE-B1A8-5BD501583221","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"1d75275853fb84ac426baf809ec86decf612055f","datavalue":{"value":{"entity-type":"item","numeric-id":651314,"id":"Q651314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$8BAEE08C-2F7D-481F-9E17-AFFA0737C9CD","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$6AB027DC-ECC1-4B1C-BFA6-C184D761180C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"250f083a2ef1e7a7df79afad0acdd22e5799ecf5","datavalue":{"value":{"time":"+2019-01-15T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4647575$AAE4B25F-275C-4AD7-85BB-98ED97E88E82","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"957970e11422fbdef7ba9db5e2b00bc9584e024a","datavalue":{"value":"03G30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647575$D78B4B59-C217-4CFE-BAAE-960EB3F66AAE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647575$125FB327-F65B-4511-A68F-BD4A247F0999","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647575$9193F178-A175-4C42-9966-6F87FEF76687","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"30f000f89c05b5d6c2fc3f4a3150ef0dac5952d4","datavalue":{"value":"18B99","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647575$5CA7D528-4FD6-4D9B-8E6A-F412E52F0A60","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"06aa1c5e457fdf637bcd3f4379f3bf7c95b0062d","datavalue":{"value":"7002049","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647575$A9EEDF22-C03B-45AE-AD5A-01E5FD797F16","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647575$00D303E3-44C9-4E63-B19C-CD8B15F477B2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9af64aff6f4b1584152e161c095f4457b67fd943","datavalue":{"value":"dependent type","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647575$E17E1E1B-05B0-4D43-BCBD-CC5B8A552556","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6a78675f0dcb3af511ac1d4dfa61901e828bcb8","datavalue":{"value":"proof assistant","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647575$886F91BD-EF70-4ED2-A7CB-BA6122AF9A5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c6cd19045b90f767537fd02880c2ebc9baafd93d","datavalue":{"value":"coherence condition","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647575$1BD2ED67-7AE5-4AB2-A646-5DF13FEC31CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ed197a229fbc0b1225e5c9b441116e253e5ce61b","datavalue":{"value":"equality judgement","type":"string"},"datatype":"string"},"type":"statement","id":"Q4647575$D15D7C5A-24E2-4598-8496-AB4789669EDE","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$74ACCCE3-704E-441D-9119-7F027633DC06","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":"Q4647575$0C381419-4834-40B0-AFF2-C94BFBF0D550","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"6bb6abc2bab9d3362ab23e392b19468def05ab35","datavalue":{"value":"https://doi.org/10.1007/3-540-61780-9_66","type":"string"},"datatype":"url"},"type":"statement","id":"Q4647575$495ACE06-46D9-45DB-A1D5-775650BE51EC","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e5d67251f45be5d91d871f99a0aa578addf3aabe","datavalue":{"value":"W1494555245","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4647575$1B2D1BC2-D731-49C1-A742-6CC41134ABE8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cb1487200638e3f9441e8913bfd2f4d0995a3fb","datavalue":{"value":{"entity-type":"item","numeric-id":3677911,"id":"Q3677911"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$891AEDD0-13FE-459D-A647-A7BE18369D48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fe2344bfb19519775177714e0f07b072be03e9f","datavalue":{"value":{"entity-type":"item","numeric-id":4647569,"id":"Q4647569"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$83A863A3-5EBC-47CD-A6EB-4ED15ECA3F3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5adae15f6654acfbcf7621f32cd882969fbf6d8f","datavalue":{"value":{"entity-type":"item","numeric-id":1096716,"id":"Q1096716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$322F0344-A105-439A-B38E-999360C455A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"730be61f324b593b9cdcf693cd18218da2ef3707","datavalue":{"value":{"entity-type":"item","numeric-id":2785696,"id":"Q2785696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$4AADDB44-CFC9-48D6-91A2-BE60D5007EEA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8eb1f5730dc671e95d2c4237dfdcada480417c74","datavalue":{"value":{"entity-type":"item","numeric-id":3142163,"id":"Q3142163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$D3005507-73F2-4582-8BCE-E78899421F8D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"48a73b0bc94774198cd192d06e32293454cda383","datavalue":{"value":{"entity-type":"item","numeric-id":4225149,"id":"Q4225149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$3A363404-C32F-4AAD-8015-DADBCD2EAC99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d6ee172cf1bbc62eabf7dd1b43feaebcac6a2fa9","datavalue":{"value":{"entity-type":"item","numeric-id":3886868,"id":"Q3886868"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$E1121217-37A1-4651-985E-78A378288FB7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0ff7991562411ba98f0f54372afaffc7b89e7d1f","datavalue":{"value":{"entity-type":"item","numeric-id":1349667,"id":"Q1349667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$6911B153-9FC1-4E52-8F64-A7182D85EDAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d33e928887af0bb982765db1d362caa615f098d3","datavalue":{"value":{"entity-type":"item","numeric-id":3325725,"id":"Q3325725"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4647575$DE91463F-B8AF-4D3E-8BB9-9D221AACF352","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27d0fdcf383e8f451027956cc909c68d5e1d009b","datavalue":{"value":{"entity-type":"item","numeric-id":2871881,"id":"Q2871881"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e5fa9b1b3da667950c0c862b1ef3aabbb88ba386","datavalue":{"value":{"amount":"+0.8405621647834778","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":"Q4647575$56EDC43A-9EA3-422F-BE81-CC9CFFCA41D7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ad8da43c5742c2daae0d692e9a46ab9ddf66ef57","datavalue":{"value":{"entity-type":"item","numeric-id":4474857,"id":"Q4474857"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"70a76d4828fc4771aebfa85a0fe5a2105fa8d3b3","datavalue":{"value":{"amount":"+0.7867048978805542","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":"Q4647575$CFC9337E-B920-4A08-AD3C-BD59AB292FFD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"718ddf24aca222678c69eebcd41c61f56bc43624","datavalue":{"value":{"entity-type":"item","numeric-id":2253180,"id":"Q2253180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"31b028c0da1cd16738f8b03e817fa908b41baf69","datavalue":{"value":{"amount":"+0.7790225148200989","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":"Q4647575$AE861811-9008-43C6-BD3E-DCC279284F4E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e923df3bf9608d52d0b963a0f393bb430f783da4","datavalue":{"value":{"entity-type":"item","numeric-id":4225149,"id":"Q4225149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6505cc1357f6637105948f6e645512b26750d792","datavalue":{"value":{"amount":"+0.7768435478210449","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":"Q4647575$CDD56AE0-B72F-4CA7-B812-C524F72611EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40811d73e7c547e0905aebe90307fb86f3415ed9","datavalue":{"value":{"entity-type":"item","numeric-id":5014596,"id":"Q5014596"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6505cc1357f6637105948f6e645512b26750d792","datavalue":{"value":{"amount":"+0.7768435478210449","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":"Q4647575$1268E0D1-BC9D-482F-BB4E-A9B7B7650BBB","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4647575","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4647575"}}}}}