{"entities":{"Q3535620":{"pageid":5565524,"ns":120,"title":"Item:Q3535620","lastrevid":50492693,"modified":"2026-01-14T04:58:28Z","type":"item","id":"Q3535620","labels":{"en":{"language":"en","value":"On the strength of proof-irrelevant type theories"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5365485"}},"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":"Q3535620$4E3B68C0-CE6E-482B-93EA-021688B8ABEF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"4b1a83da939f8ed2c959070ccb001de4e48a6f06","datavalue":{"value":{"text":"On the strength of proof-irrelevant type theories","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3535620$D15065C4-CBF2-4812-8572-1EAB8376F539","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"8a1138d814b8e414c0fd69e0401b451b4d5101b8","datavalue":{"value":"1151.03317","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535620$16360A46-C9A3-4D22-B837-1120D82A46A1","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"08a36a966fe34dfd9695800e38475b4761f56386","datavalue":{"value":"10.2168/LMCS-4(3:13)2008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535620$BB654E61-7E8B-47DF-98E4-98B53EB25AE8","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f69fec18e304e301a38c349c8b21d1a76ec69093","datavalue":{"value":{"entity-type":"item","numeric-id":1322846,"id":"Q1322846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3535620$7D3B3313-D7E2-49DA-BCFC-C1C167F464CC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"da58c52dc46c86e7440f2499c9e1bef3537c5562","datavalue":{"value":{"entity-type":"item","numeric-id":2786118,"id":"Q2786118"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3535620$870FAFED-7FE6-4E28-9E6E-0A99D7B4276D","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"27f25e9d3b3894d698b7ec67f164a27a3aba1f7c","datavalue":{"value":{"time":"+2008-11-13T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q3535620$DBC4A609-4F9D-4581-8BB3-AF0419ED573F","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"dd8503cb84d44ac2adb520ebbb11872e6dc1ec3b","datavalue":{"value":"03B15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535620$6F575CC8-D12F-46F8-AB24-C10180D76004","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535620$F1CB59DC-03AE-4A42-BC9B-FE19CC1D62D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535620$A3A614EF-BAA6-4EDD-904B-3ADA0CA82DA0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535620$7ED2D563-0907-4560-8015-752DD08B4ACC","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2da2a4139e431ff5a22c1f36d7e45bd45e569d5e","datavalue":{"value":"5365485","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535620$D95D9783-597C-4FC3-9A9E-D5202F6E0515","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e13bc8441d7666d4310a93839316ebef38c603a6","datavalue":{"value":"prototype verification system","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535620$EF846FE2-E3ED-4D9D-9017-6CDD8C0249F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535620$1A24798A-5622-414A-BEB3-819E3ACF2EE5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535620$4AA05BA3-AAE6-42AD-A1F8-9FB86884C10B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"369d809faf45cd7c2feadd7217eb1a0d072ebf93","datavalue":{"value":"proof-irrelevance","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535620$C806EC3B-DCFE-4269-8B7A-A4C434D7C0C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"260d20bcdb0b894f57a6beba756287ebf28a84d2","datavalue":{"value":"conversion rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535620$A92B3A19-6471-400C-9BF6-BEB4ED005A1A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9b3672fd7a26fc0111c32eced7b0c9350b9638f3","datavalue":{"value":"additional extentionality","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535620$8F50E5E4-2BD9-4AC6-A3BF-0E7C023F907A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0836092e1fe2f2c9bcc68cbbaa259608b2f6de67","datavalue":{"value":"axiom of choice","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535620$30D1B289-A2CB-4C80-AFB3-93BB3990DCD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1286c13c664f7fac6cfb71e87e1b3d43fbdcc933","datavalue":{"value":"set-theoretic semantics","type":"string"},"datatype":"string"},"type":"statement","id":"Q3535620$B1CE7AA2-9111-4CAA-9E8E-B2DED643AD45","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3535620$6314A0F7-01E8-484E-8A07-44005172090A","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":"Q3535620$A8E2F9D0-F1C8-4219-AAF6-1102CE668EC0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8bdfc433dd677fa326c2980cb4dfa4e0c1047711","datavalue":{"value":"https://doi.org/10.2168/lmcs-4(3:13)2008","type":"string"},"datatype":"url"},"type":"statement","id":"Q3535620$ECD523E2-9182-4A76-B274-E9F1EC8AC978","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"44e7e7dcde8bb33e6218d0d0afae5960dba2500e","datavalue":{"value":"W3101932690","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3535620$23B213CB-90D2-4D81-A7B4-8E4F4F98999C","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0374978b71ce4f934a36d4ae8d192493815b5b6c","datavalue":{"value":{"entity-type":"item","numeric-id":3613437,"id":"Q3613437"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a34bd45262ae2e8faf4f8731196edd025a43b6ae","datavalue":{"value":{"amount":"+0.9947025775909424","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":"Q3535620$E2752E37-9E2E-4178-8011-F2C8043C03A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b1e3fef7a91f717d982de5af60bbc76f7514a80","datavalue":{"value":{"entity-type":"item","numeric-id":4944846,"id":"Q4944846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"221b49dbc486b7025e18ed6f00e108abd23e1a92","datavalue":{"value":{"amount":"+0.750351071357727","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":"Q3535620$DEB9B7BC-2296-4D39-BE86-6914723D4CE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6bd2a7c5ae41bbaf82e6faeb8738632585b8325c","datavalue":{"value":{"entity-type":"item","numeric-id":2176677,"id":"Q2176677"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"221b49dbc486b7025e18ed6f00e108abd23e1a92","datavalue":{"value":{"amount":"+0.750351071357727","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":"Q3535620$CE952906-816C-482E-A8FF-1E2A72CA2154","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5de30d754af82d7575c5218ddb8f50be80efb2ac","datavalue":{"value":{"entity-type":"item","numeric-id":2881097,"id":"Q2881097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"642ec0c01fc0c83f887a10809391f54cdcba3994","datavalue":{"value":{"amount":"+0.7360647916793823","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":"Q3535620$FED05364-873E-45F1-B16E-D143B7E93AA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"09b6bc96852a3f96ef80253f516081e59b013060","datavalue":{"value":{"entity-type":"item","numeric-id":661282,"id":"Q661282"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"42fb060a2d049b5768ab3e48e6b5d8a7d31fac2e","datavalue":{"value":{"amount":"+0.7344216108322144","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":"Q3535620$7BF0E29F-489A-4F12-A6E3-2CB10F8A9A3C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:3535620","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:3535620"}}}}}