{"entities":{"Q6879482":{"pageid":20773450,"ns":120,"title":"Item:Q6879482","lastrevid":84216293,"modified":"2026-05-13T17:13:06Z","type":"item","id":"Q6879482","labels":{"en":{"language":"en","value":"Controlling unfolding in type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8140615"}},"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":"Q6879482$6BF7036B-E7FD-4AAE-9E59-CE170C471E41","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"49f52f964ffd23af055a1c2a1c3bfd05033d297a","datavalue":{"value":{"text":"Controlling unfolding in type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6879482$290F4A7A-6E24-4676-ABD3-2B2F1BE4FEF9","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"2d991e295b4836169ccaffacef319ae7d06ebbcd","datavalue":{"value":"10.1017/S0960129525100327","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6879482$DB3C59BF-55B1-41C5-8BCB-1F7DD0ECAE88","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"688ab5914c55cb17c5dce51a440b79b1611d2ba2","datavalue":{"value":{"entity-type":"item","numeric-id":5072608,"id":"Q5072608"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$064446E7-F8A0-4F7B-AE55-833C9AF2376B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"612a55672006eb32b94e9a3be5b3448080647058","datavalue":{"value":{"entity-type":"item","numeric-id":5016214,"id":"Q5016214"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$FE5A28CB-2A0F-4593-AD01-DD9A4D5B0F5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3791877866e06c575a0d5afd18962bd487776b6c","datavalue":{"value":{"entity-type":"item","numeric-id":1688953,"id":"Q1688953"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$CC450EDC-0FB5-46B0-88D7-A8D680A3C0FC","rank":"normal"},{"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":"Q6879482$F5F0EEE9-EF8C-417B-ABB4-8BEC56FFB355","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"573e97e485dc7f23b42802228edbcbd518cf2ea9","datavalue":{"value":{"entity-type":"item","numeric-id":444497,"id":"Q444497"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$C831E709-DA4B-4AEB-93CA-522CE4506504","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"a53527e88e2413966f3c8ce14c92b878c452756d","datavalue":{"value":{"entity-type":"item","numeric-id":2709784,"id":"Q2709784"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$5012D9EF-EE91-4BC9-8642-3A88C53D4072","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"11cbd9a6b07c2381cdc8b09e4439c018c2b94d2c","datavalue":{"value":{"time":"+2025-12-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6879482$E62219B9-CEB2-4895-A8FA-E16D5BD8FEE5","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6879482$560DE6AA-6F81-436A-A7DE-73A8ECB2BB62","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"7cf0904cd30164ea19d1aa0871b16800746ab137","datavalue":{"value":"8140615","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6879482$B1D4C928-443B-4F2E-8334-87D0CBA1EDFE","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":"Q6879482$1BF59100-176F-426F-8D6F-D8D0DECB3FDB","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13fd823fa813aa32375d6c4605d9195c2318674c","datavalue":{"value":"dependent type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6879482$019146F3-F7B8-4020-A378-562DA8E2433F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q6879482$9410BD13-FCCC-4FE9-81B2-F4C1FC4F7B06","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6d03b8a8130479923e5c0193cc5c7481d82c09e4","datavalue":{"value":"categorical type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q6879482$44160A2D-F2C4-4212-8044-41BE5FAE456E","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":"Q6879482$3E771A7B-78E7-4F9E-B6E8-3C7A1316CE32","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f38b239c038c6ea45cf6d83346efc7512ad720a8","datavalue":{"value":{"entity-type":"item","numeric-id":5164724,"id":"Q5164724"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$2208EAAA-AC22-4312-8974-84CC3E6D458D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6f6f04e0829cea3174d08000975cc9f5ac02599","datavalue":{"value":{"entity-type":"item","numeric-id":5022926,"id":"Q5022926"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$A511EC94-FEE5-4D8D-B97F-DD363B0C2CA5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e3196c52ecefe6bbfc4fe1f8084810a6dceb61cc","datavalue":{"value":{"entity-type":"item","numeric-id":5079726,"id":"Q5079726"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$33A953C8-B1D7-4B95-AB1A-8EEFA8342F44","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eff1fd92245df38d7ffeae1e590de1b0d5007c30","datavalue":{"value":{"entity-type":"item","numeric-id":4474826,"id":"Q4474826"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$EE72C17A-E468-4ACE-8DE2-EBF9BE786D4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d16be83a3de54bd2c3181fc2cf1831e46861bc49","datavalue":{"value":{"entity-type":"item","numeric-id":3130300,"id":"Q3130300"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$82C36EF4-23D2-4DAA-A90D-22A5C924E7BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a765e855228292779b4203bd15443a2ad99c5c33","datavalue":{"value":{"entity-type":"item","numeric-id":5740406,"id":"Q5740406"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$BBBD2D27-EFE5-4A36-97B2-8939F5247CFF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6224dd9008c6167ab2abbf67da65d1f726ff5d94","datavalue":{"value":{"entity-type":"item","numeric-id":1916364,"id":"Q1916364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$1D1F67B4-BEFE-41DE-83CB-C2988C27D0B9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"27b65f6891253ffab6c51da3cf95e87aa1f1fbff","datavalue":{"value":{"entity-type":"item","numeric-id":2942929,"id":"Q2942929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$CF54DDC3-1C34-44BB-A8D8-7AAF9BE83889","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":"Q6879482$3AF244A9-8226-4C4D-9D4E-8B60402E4FF5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9e9a0da0cc8056c9fe663fd27ba6ac0a98b41be3","datavalue":{"value":{"entity-type":"item","numeric-id":5889884,"id":"Q5889884"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$CEB9F52D-2E5A-499F-9E47-3403374FF7B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d036040bf3ed5c2e1ffac6f62b9b04d9e598837b","datavalue":{"value":{"entity-type":"item","numeric-id":5665316,"id":"Q5665316"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$16E145B6-6DE8-4CA3-BA7F-E299ADE9C4C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f27fd93c1b5d93bcea3172146c72a26a046a3b1e","datavalue":{"value":{"entity-type":"item","numeric-id":2319982,"id":"Q2319982"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$526BE0E4-6A28-481C-BE92-B5B324E4B851","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b38e8a5f05f471c9700346854042774609226b3f","datavalue":{"value":{"entity-type":"item","numeric-id":3196351,"id":"Q3196351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$A81AB1B3-01DA-473F-8F65-27232AF78492","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae56cbc30bf4e0ace39780e420d931108cdd0102","datavalue":{"value":{"entity-type":"item","numeric-id":4145861,"id":"Q4145861"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$C5E37F02-BD29-4B18-898C-A6438C36C320","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d1a86a2916d0db0c2fd5d3c89f43e0f228fe085b","datavalue":{"value":{"entity-type":"item","numeric-id":4281477,"id":"Q4281477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$B27D44B9-A047-417D-92A5-D6F0D76F92C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"707b5ac070fb8bc02a181197aa4b08e8edc80bc4","datavalue":{"value":{"entity-type":"item","numeric-id":3400012,"id":"Q3400012"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$712A4A91-DA8D-40A6-AA98-1ABC7F45CDA0","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":"Q6879482$594B9753-FDE7-45FE-BE2B-0251239A9B00","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8eff01d0710054224f955bac4bb082ed40f5e8c8","datavalue":{"value":{"entity-type":"item","numeric-id":3121017,"id":"Q3121017"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$CCBE92B5-395C-4670-86BA-EF300A6D99AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a0f377b770c16a2f11d17da0cc7de086af5c0ff4","datavalue":{"value":{"entity-type":"item","numeric-id":6911852,"id":"Q6911852"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$B7B5BADF-0B92-4561-93BA-8E62963B62DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2304fc249104140bc982b97cc610a3c2e3999c7d","datavalue":{"value":{"entity-type":"item","numeric-id":5056429,"id":"Q5056429"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$BD54405B-6CBA-401F-8264-B144B0FD9588","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69fe664aa22c6ba1ea6d9ba12c2b4c3da0298ee2","datavalue":{"value":{"entity-type":"item","numeric-id":5277760,"id":"Q5277760"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$7B15F905-272C-4595-9033-1DECE608E2C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"61bc750c8271299b673749bc2030f9e5ed6735ce","datavalue":{"value":{"entity-type":"item","numeric-id":6149910,"id":"Q6149910"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$8E5F28FE-CFE8-4940-8316-E9015A4DEA78","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"890522dc4e3ecb3007fccfde8c53acf4163b6c1a","datavalue":{"value":{"entity-type":"item","numeric-id":5420262,"id":"Q5420262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6879482$71EE5F70-7C6C-47DA-A4BE-FF3907DA1922","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Controlling unfolding in type theory","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Controlling_unfolding_in_type_theory"}}}}}