{"entities":{"Q6083893":{"pageid":13218200,"ns":120,"title":"Item:Q6083893","lastrevid":94072604,"modified":"2026-06-05T05:48:35Z","type":"item","id":"Q6083893","labels":{"en":{"language":"en","value":"A short and flexible proof of strong normalization for the calculus of constructions"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7774797"}},"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":"Q6083893$FAB7782D-611B-472B-9576-DDB622BBB84D","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"fe8aaca24903449bb87560a77616bc6e59dd1e4f","datavalue":{"value":{"text":"A short and flexible proof of strong normalization for the calculus of constructions","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6083893$E2896DF4-8C29-4414-A3BA-F8DC9BC2ED02","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"10577b7a039aae8e822245055eae09f7f239fae2","datavalue":{"value":"1530.03058","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083893$D9E18D77-6ACB-4AF9-B371-11CF4736A8CB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"1a9cc5f0ae66c585c50f53258bcf0c2576831b08","datavalue":{"value":"10.1007/3-540-60579-7_2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083893$A2459AEF-665E-4673-8F8E-6DD4E2212561","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"d617c217f8f04ef480d650a973c1ec01fe67123b","datavalue":{"value":{"entity-type":"item","numeric-id":235622,"id":"Q235622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$F599B10E-0119-4197-8817-47730861C8CC","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":"Q6083893$7425980F-02A0-433A-B860-8490E4FB5601","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"80837e4f107d88dc61f75b08f8b7aa1a590aa151","datavalue":{"value":{"time":"+2023-12-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6083893$60DD122B-4F25-42EB-8550-1FFE29646FE8","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"fc167512df1c01ab112ff06096544314dc6ac625","datavalue":{"value":"https://research.tue.nl/nl/publications/3619121e-2a08-4571-80a7-0eabbc7a4f7d","type":"string"},"datatype":"url"},"type":"statement","id":"Q6083893$7734CFB6-BC82-4B68-88A7-BF26AF533A9A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083893$D5F4A8B7-6646-4F35-805E-905606725BC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083893$D4EEEF98-9173-4D93-BA8D-BC8E0CC5BC78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083893$F477A0DC-58A3-4076-8935-3A63D22FD19B","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"437be4e8b9c7154fa92df716931906ad5ad51625","datavalue":{"value":"7774797","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083893$189F84E1-8B35-4082-9170-C2F721A221F2","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ed28ff65c7143ccab364c3b93115be1e84f3431a","datavalue":{"value":"inductive type","type":"string"},"datatype":"string"},"type":"statement","id":"Q6083893$B2556698-3C76-49CB-8BDE-ED92FE2F9912","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"69eaa0b39db33bdfb90e0e2fdc84d350c2fd3843","datavalue":{"value":"type constructor","type":"string"},"datatype":"string"},"type":"statement","id":"Q6083893$B27AE172-629A-4F38-B137-E483A87AABB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"af462e56ed2ce88a42c8df0ec7f2dc6a55ded212","datavalue":{"value":"strong normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q6083893$E91D7837-EA9D-4367-9422-3DD6E987F9D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"260d20bcdb0b894f57a6beba756287ebf28a84d2","datavalue":{"value":"conversion rule","type":"string"},"datatype":"string"},"type":"statement","id":"Q6083893$BB09FAC1-BBCB-4F3D-96D8-43639E3AB82D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"156147248c5524d3c5be75e84327ccf20aae86f7","datavalue":{"value":"soundness theorem","type":"string"},"datatype":"string"},"type":"statement","id":"Q6083893$6C890E5D-157D-453B-AA7A-0DAF3C2E614F","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":"Q6083893$62C974EA-37D1-4475-9E45-49B6F032DBEF","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6d8bc9d1b50908ce3abd5cf70ba3d7d27f3fb3e2","datavalue":{"value":"W2103033459","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6083893$5D4E22A6-7419-4685-AF0A-3419AA4710C8","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a3bd3ba10b0a8db4c435a1f311674675f6385e0","datavalue":{"value":{"entity-type":"item","numeric-id":4234771,"id":"Q4234771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$5BDC3F7C-BF43-4B2E-B662-3ACEB7D8AE75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"956c663a8c65ca7a493106b21f9b04a9a741383f","datavalue":{"value":{"entity-type":"item","numeric-id":1155602,"id":"Q1155602"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$0BEB8232-52B5-444B-B528-A8B801B358E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eabf8cee824c9a4fda7f420caf89018796ca96d0","datavalue":{"value":{"entity-type":"item","numeric-id":3889024,"id":"Q3889024"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$12258B07-FA58-4FC3-B2CF-C98A7F876D98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d592f87e8857ff4d106dd1dd178161f50c9229b","datavalue":{"value":{"entity-type":"item","numeric-id":1108266,"id":"Q1108266"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$AAF557DC-71A9-4A20-854D-8CBF9EE132E4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ad80344fc1eac9869a64dbac310f2d1dda233df0","datavalue":{"value":{"entity-type":"item","numeric-id":4939698,"id":"Q4939698"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$9E6EA674-D6B1-46EE-913B-02C848C113D4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1c7ab0bef98f3dafd356831c56f39b6e31577416","datavalue":{"value":{"entity-type":"item","numeric-id":3612441,"id":"Q3612441"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$64E34BD0-60DF-4EA0-A743-EB458F24FB2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"99c6176bcb92cea3bde43c51d54f8875f446d09c","datavalue":{"value":{"entity-type":"item","numeric-id":3994895,"id":"Q3994895"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$24389584-F160-415D-8FC5-0CBE3B999C6C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e04882dd0098e511c274267f86b00f5c3a4c9815","datavalue":{"value":{"entity-type":"item","numeric-id":3211296,"id":"Q3211296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$A5489CE6-FE63-4EBC-AB76-5D0DD6F53FB4","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":"Q6083893$2F5F2932-0710-4237-BD74-4074E2E6F480","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3ab5d7b35f67f940445411fa45c1b02bcb40d39f","datavalue":{"value":{"entity-type":"item","numeric-id":3999860,"id":"Q3999860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$78F53674-E87A-4F12-8C69-CEFC4397D736","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"07e6add6d7e4f9b356a84d7914f4cae03cd3f03b","datavalue":{"value":{"entity-type":"item","numeric-id":4525289,"id":"Q4525289"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$1DB0E311-8CF4-4D2A-A498-0FD90E056DEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8522203069c662f42e96bc0d7df3b0c3af526a7a","datavalue":{"value":{"entity-type":"item","numeric-id":5533180,"id":"Q5533180"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$5FC8E569-6A1B-4683-94C1-8A162B36ACD1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9bd4384e04df05a6d681d8752a6931ccfe2df646","datavalue":{"value":{"entity-type":"item","numeric-id":4093416,"id":"Q4093416"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$2CB11A67-20BB-4491-9C77-89A632844D0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e195a519ca02237c87426a6e69de956fcb956d38","datavalue":{"value":{"entity-type":"item","numeric-id":1891251,"id":"Q1891251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6083893$1675C000-4C0D-4DC8-8CAB-8EF13B65C1E0","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A short and flexible proof of strong normalization for the calculus of constructions","badges":[]}}}}}