{"entities":{"Q2311883":{"pageid":2322626,"ns":120,"title":"Item:Q2311883","lastrevid":56658933,"modified":"2026-03-18T11:32:09Z","type":"item","id":"Q2311883","labels":{"en":{"language":"en","value":"An adequacy theorem for dependent type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7076765"}},"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":"Q2311883$81A785F6-3A26-4494-8260-988C169AD495","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"406c9e65e9ea1f91b15832de84eaca06a55f0afd","datavalue":{"value":{"text":"An adequacy theorem for dependent type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2311883$E8DA5054-E3C6-4566-9AB7-CBCB304DE14D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c5dfa7fa4073aea33271e8a99c0c885a4a242f66","datavalue":{"value":"1454.03020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2311883$837F61B9-4A41-4531-A47C-4494C59E1FFD","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5aad179d365c253d181fa8115a831f46e7923370","datavalue":{"value":{"entity-type":"item","numeric-id":375196,"id":"Q375196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$1C3B66C5-EA56-4D1B-8B70-B201B386E533","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"14376caa07db3f1fa1adc4be796c3dca3ec648ce","datavalue":{"value":{"entity-type":"item","numeric-id":2311882,"id":"Q2311882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$D79FDE58-D704-4E5E-B2BC-3BFC8AC58586","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b559743f011d61696dff04b2ecd3408df2541e49","datavalue":{"value":{"entity-type":"item","numeric-id":169698,"id":"Q169698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$00FBF793-1AC5-42B5-9C31-84879C7D8D38","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"311afef0a4b95245df7f6c2908ad6e9d40f3f2be","datavalue":{"value":{"time":"+2019-07-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2311883$B95E69B8-3ED6-4465-BED4-78E19212E6C6","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2311883$1A312A58-22CF-437B-9B14-CDE8F63363A1","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"5d3c2a7e793546089ad289125ef3f11485345851","datavalue":{"value":"7076765","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2311883$7D1AEB44-2F21-4467-8B0E-4B7FBAB21A12","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2311883$5283A58A-47A6-47DB-8CFD-F8CE20487915","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"40443e796d30a9a7c10499432df73c84da618b03","datavalue":{"value":"domain theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2311883$483A5172-E3CA-4CB0-8E62-58BCF6E73595","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"7e08b5081fa47443be725d8e77558cc610080b17","datavalue":{"value":"finitary projections","type":"string"},"datatype":"string"},"type":"statement","id":"Q2311883$33567A1C-F0DD-41F1-BC0D-A3A547807447","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":"Q2311883$F8DA26FB-C828-4CAA-A48F-B6FB65A36DAA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7d306d5eb1c57774bc5e7f3d1b281d1c83f8edf6","datavalue":{"value":"https://doi.org/10.1007/s00224-018-9879-9","type":"string"},"datatype":"url"},"type":"statement","id":"Q2311883$C1FFB4FF-58F5-4E2E-BBBC-A3AABC147615","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"573292ca0e35fbd0c714199accdbfd96b426d1f8","datavalue":{"value":"W2883606308","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2311883$0DBD651B-C4F4-415C-9144-D6463FB89734","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"833079337a3c2f303ddbc3fe894c26799c99160e","datavalue":{"value":{"entity-type":"item","numeric-id":2881097,"id":"Q2881097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$AF14D806-0C22-446E-A348-60C02CC86368","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"590bafa3f5ab2539f54e87a74876e71f860845ef","datavalue":{"value":{"entity-type":"item","numeric-id":3377462,"id":"Q3377462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$96616B0B-A597-4F08-B280-02C8FCB312BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27e31b151b8d22be2aa79bf2dfac73aa834ed045","datavalue":{"value":{"entity-type":"item","numeric-id":4012882,"id":"Q4012882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$ED279856-3656-4151-8D0F-7CE113834A0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de30bc71fa2f80f80d10bc8645b2c869132c82fa","datavalue":{"value":{"entity-type":"item","numeric-id":1824612,"id":"Q1824612"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$41FBB7D5-1BEC-44ED-8CB6-4E442102BD98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"009122af7eb8e6ecc8feb2892d4b88e663912c90","datavalue":{"value":{"entity-type":"item","numeric-id":3328540,"id":"Q3328540"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$7DD9F514-D669-4559-9700-1DA8B3E5630F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6956a12199d710944333687ed9f973870967e27d","datavalue":{"value":{"entity-type":"item","numeric-id":916656,"id":"Q916656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$32D051DA-4776-4E95-853A-8765CB9D4190","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a0bb0ad006a2dbf080650d414f85c549f8a73b32","datavalue":{"value":{"entity-type":"item","numeric-id":688734,"id":"Q688734"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$DB6F14EF-AED7-4FC9-9608-275ADA9FE061","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"573bf50881a638b8d1bc1330f0a3383e6e028b45","datavalue":{"value":{"entity-type":"item","numeric-id":4072829,"id":"Q4072829"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$EEA7AD94-AE44-4E63-8576-E08A3AA2DA0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"334057c9297d6a0878784b79f130fef6a1b466a8","datavalue":{"value":{"entity-type":"item","numeric-id":3110202,"id":"Q3110202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$EB5745AC-6F10-4C2C-9C3C-2B884B3A792E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"681f6b991823ef1eb2ae5a0dc4952d80f163b9df","datavalue":{"value":{"entity-type":"item","numeric-id":2844696,"id":"Q2844696"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$82657492-891E-48DB-BD3D-FE843DF38E7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cd2973a40cdc7ada8d04704b32ff80bbdfecef18","datavalue":{"value":{"entity-type":"item","numeric-id":3960746,"id":"Q3960746"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$727A05F1-3718-4289-8910-07C9C1DDE480","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"467d88d94bfdf476c0f82dbff194f0ff1beaea57","datavalue":{"value":"10.1007/S00224-018-9879-9","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2311883$2FF9CE77-00C5-449B-95D4-5DE0DC30D79E","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"70d1c0c60e818a25e44291ff02327303f50c8922","datavalue":{"value":{"entity-type":"item","numeric-id":1306706,"id":"Q1306706"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ff998499084acbc513357cf35ab281cbebde460e","datavalue":{"value":{"amount":"+0.763873815536499","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":"Q2311883$10925FB7-5584-4904-B399-65E4FAB6EE0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"69c627492fd500f9c724d36db9e0f420687d667a","datavalue":{"value":{"entity-type":"item","numeric-id":4247302,"id":"Q4247302"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3fdc9acc7a1946109ebecc167482c15f7d1f64ff","datavalue":{"value":{"amount":"+0.7476398348808289","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":"Q2311883$7BF9EC0E-C648-436D-A5DE-69FB6ACB092B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5348f7970ff00c39fd4396ee481e25d5114de055","datavalue":{"value":{"entity-type":"item","numeric-id":4006238,"id":"Q4006238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3fdc9acc7a1946109ebecc167482c15f7d1f64ff","datavalue":{"value":{"amount":"+0.7476398348808289","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":"Q2311883$76DE1A55-364F-4945-B425-128D55165F30","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":"fddcc4a918651f5030530e8564aa698d6a6114d4","datavalue":{"value":{"amount":"+0.7419371008872986","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":"Q2311883$93F98194-EB39-4AA3-A310-C48CE9D9B096","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a1688790b6bb9794dc307ab64199e60b9d1109d8","datavalue":{"value":{"entity-type":"item","numeric-id":3449463,"id":"Q3449463"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fddcc4a918651f5030530e8564aa698d6a6114d4","datavalue":{"value":{"amount":"+0.7419371008872986","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":"Q2311883$40AED6C5-10C1-4A9D-AACB-AF593FA96EEC","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2311883$556387CE-B126-4E72-A09C-8C943405F12B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2311883","badges":[]}}}}}