{"entities":{"Q2422026":{"pageid":2432769,"ns":120,"title":"Item:Q2422026","lastrevid":57908694,"modified":"2026-04-03T01:18:09Z","type":"item","id":"Q2422026","labels":{"en":{"language":"en","value":"Canonicity and normalization for dependent type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7067587"}},"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":"Q2422026$8EA33718-AEA9-4667-86DD-4D1D29AB57AE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cf87fbac46990b2995ce729faf1b9333c289b6d5","datavalue":{"value":{"text":"Canonicity and normalization for dependent type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2422026$5C2D5F0B-9DC1-4B4E-9355-81947F2A95EB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"6c151a4babedc279069e62993308e4a402c2a223","datavalue":{"value":"1454.03019","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2422026$02BCE501-069E-4F0D-A5AF-D0F61ECD4F71","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":"Q2422026$07E4EB75-4EDC-4D34-B68B-C14BEB3E8344","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$9C47145B-8E3B-4766-B1DF-E1524F3E03A2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"001edf23e586a650fb6b34425b0aaf644eda2260","datavalue":{"value":{"time":"+2019-06-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2422026$3AF2E320-C920-430E-8562-3266155BA9FA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f4ff0822e32d252a7df643a3991974b83b5ea461","datavalue":{"value":"https://arxiv.org/abs/1810.09367","type":"string"},"datatype":"url"},"type":"statement","id":"Q2422026$C171E6DB-1751-4603-BFBA-CFF8AE463C78","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2422026$0E1D944B-D2FA-4675-B1DA-D452F9CAC66E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2422026$E2990F06-0F98-46EE-9A9E-99F19B85AC7F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"2aac8faaf7cdd995b10160bc468357bc72d52213","datavalue":{"value":"7067587","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2422026$25029CAA-E636-4C69-835D-41CAC7770576","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2422026$C1ACC077-3E44-49AA-B527-2A2DCC609F6A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"190d3af93d3a3fc40ca0ff5196125ddd6cbee0e5","datavalue":{"value":"normalisation proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q2422026$28C5812F-359F-4D88-B1DF-82BAE4B8EA47","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8026960d6f36428821b4502bc1641829b1806e7e","datavalue":{"value":"higher-order abstract syntax","type":"string"},"datatype":"string"},"type":"statement","id":"Q2422026$85DF35D5-2C56-4E65-B034-943DED0E4492","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b29eb58b948f9f996cbb5eae736ddbdaf0434b06","datavalue":{"value":{"entity-type":"item","numeric-id":34514,"id":"Q34514"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$93985C6B-E85D-4B6B-9CFE-7CB6AF2EAE9B","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":"Q2422026$5D65E23A-F66E-42F0-9DE1-D6FA0A6E745C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"2f1e10048745436f6f29b91018ab39867344b61a","datavalue":{"value":"W2963765784","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2422026$49B98345-66B0-4818-94FF-32A8CE543A29","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":"Q2422026$ADD9B29B-D4A5-4BF6-9E47-9A7E6D11D41A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ee1bd5723754d3f3766daaae49b37c3f6d620266","datavalue":{"value":{"entity-type":"item","numeric-id":4944846,"id":"Q4944846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$99FF2583-C800-4197-9EAD-CD157017B7BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae01153faff5da16cf5c80d9e744dac606c437f0","datavalue":{"value":{"entity-type":"item","numeric-id":5369471,"id":"Q5369471"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$23B85C2E-5382-4A35-B69B-7E8599D611AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e154aa9118f1cfec335fe4b3f0ee878903e59e9e","datavalue":{"value":{"entity-type":"item","numeric-id":5176953,"id":"Q5176953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$0CA6598E-F75A-4EED-80EF-9A90362C8571","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":"Q2422026$16DA23B8-7647-4238-9C3C-1FE424809E94","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"36966a8e78b7ca52795d4f824a4634dc030e8550","datavalue":{"value":{"entity-type":"item","numeric-id":1612481,"id":"Q1612481"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$B9E7903F-C683-4A96-A0A1-3CF95AFF12F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e544e438e6837b40684be8afb567ee872639a802","datavalue":{"value":{"entity-type":"item","numeric-id":4647575,"id":"Q4647575"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$6BB0BFC5-1DC3-4F05-A5B5-0353BEC4A92C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"53bcfabc22212d3db2a4fa41c3566844e5ecdda6","datavalue":{"value":{"entity-type":"item","numeric-id":3668859,"id":"Q3668859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$C5F78AD6-089D-4E39-84B3-B97C4ECFEB83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d357a47c04e8c031646a6927518ecdcc37982e0","datavalue":{"value":{"entity-type":"item","numeric-id":3262780,"id":"Q3262780"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$1E43C6EA-3311-4D6E-A9C6-32F8C551AE8E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d82b227295c10b6c3c9289b01dc8016d6c611441","datavalue":{"value":{"entity-type":"item","numeric-id":3727946,"id":"Q3727946"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$205D77E6-6320-487A-BB48-057E425A73E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae94f828af67e50fecbc9e4b645ed6964977b9db","datavalue":{"value":{"entity-type":"item","numeric-id":4099613,"id":"Q4099613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$5CEC1758-C4C9-4744-8F87-5BE4068BDC10","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"72bce0021a20e6075192b92537623e64018b293b","datavalue":{"value":{"entity-type":"item","numeric-id":4099614,"id":"Q4099614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$AEF25897-23CF-4777-B9AE-C7885DE27044","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":"Q2422026$D5C040F8-072F-4A4B-8BDA-D929B510DE28","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3f40bcaa8d311e4db512eab174f3dec9cd00f54c","datavalue":{"value":{"entity-type":"item","numeric-id":5537599,"id":"Q5537599"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$26B47262-EB65-4D34-AC3D-1D2CBFF3E40E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"472fe6e79b503d14429d15ec73a6169d7420ec0b","datavalue":{"value":{"entity-type":"item","numeric-id":5740656,"id":"Q5740656"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$0A8DC83C-CFE5-4C1A-B189-76F9F413C788","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3c7130b8e8ad403bac4e3a609004e5598d1175d3","datavalue":{"value":{"entity-type":"item","numeric-id":5561939,"id":"Q5561939"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2422026$6C5C7212-900C-4916-A8A5-BC3DE7013545","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"d3891e8e02d63acac5ad37171324276783fe117c","datavalue":{"value":"Q128559732","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2422026$59F67D10-C1C9-4C7A-8CDF-19155F382B40","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"9045e6458e0c0591507f2ece2682ce133aac70d3","datavalue":{"value":"10.1016/J.TCS.2019.01.015","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2422026$3E27B78F-D782-467C-B89D-24CB2B681E15","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2422026","badges":[]}}}}}