{"entities":{"Q2333314":{"pageid":2344057,"ns":120,"title":"Item:Q2333314","lastrevid":71868921,"modified":"2026-04-14T01:04:42Z","type":"item","id":"Q2333314","labels":{"en":{"language":"en","value":"Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7128694"}},"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":"Q2333314$54D18948-8624-4124-9E8A-858806CD40BB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1818b46db3d0e8f673e1c92b8cb77671240c1d26","datavalue":{"value":{"text":"Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2333314$D8C1E547-A401-447E-A49B-7DC752195965","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"56a3c2231ceed2f8d5623e060c48f3a14d1eeed2","datavalue":{"value":"1433.68542","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333314$0399B56E-6DB3-4EA5-91CB-0CDD149B43C3","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ef5f2fcbe4affe3a081b63bc32cd9f9b1ef1904f","datavalue":{"value":{"entity-type":"item","numeric-id":530863,"id":"Q530863"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333314$E91B9ADA-EFDB-4757-84DE-55F8ACE14B0C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"402a48fb715d415da55853e3651509e9510c9149","datavalue":{"value":{"entity-type":"item","numeric-id":220715,"id":"Q220715"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333314$A78C53B3-5BA0-427B-9451-D5BF81765F0F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"746409b166da6b3324f8a076651b3e33b41a949f","datavalue":{"value":{"entity-type":"item","numeric-id":530862,"id":"Q530862"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333314$CA5B7E2F-B4BC-411B-909E-376F391F91A2","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"38a671beb2eece257f68ae67ea5951ace27cbec7","datavalue":{"value":{"time":"+2019-11-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2333314$2FE87CC3-2756-4E2C-871C-6727EDEAE572","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333314$7519913B-0DD8-4234-A222-230FF71A9360","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"10eaeaf8bbf8231bbfc812aab8956e260b5a9f12","datavalue":{"value":"03B35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333314$50BA0396-F00E-42F3-A28F-B85395336342","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d9230c8da6e5632ad621620269b7ca185454f9df","datavalue":{"value":"03B38","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333314$6C54E6D6-4F41-480E-9709-376AA3FBCE54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333314$DABB82E0-AA27-4301-9429-526780D13CA8","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"71d4137b8f5b25c1958284f3d4c0ad6a56035aa3","datavalue":{"value":"7128694","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333314$80B191F0-025E-4B1F-ADA6-7E972C2F7E3F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333314$4494D7DC-38BB-4E44-8EBB-EEB716296132","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"34ae3a8d9f3401a083509ec6ab2b6f0f2deb2a29","datavalue":{"value":"formal metatheory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333314$DD8E30DF-895D-41CA-BDAD-DB2DE2DFE687","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ea0e35eece84bed33461e424b92d07e45bd0c24","datavalue":{"value":"type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2333314$51D4C555-2BA7-4E91-95C3-C156A5F4439B","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"cca90c8b2497d1cb8f188a28d5c668cfa22022b4","datavalue":{"value":"Q113317509","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333314$67B89848-6816-41A4-9B6D-7CE46AD0FF66","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1a8b6b13bef47cb19f4e2508b5917af235a65eb0","datavalue":{"value":{"entity-type":"item","numeric-id":21668,"id":"Q21668"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333314$531DAF05-1C0D-49CE-AF5E-184D80ACC116","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":"Q2333314$14C9CCC2-388C-468C-88F3-A5F61C97E3A0","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"47df37c4e7ef96cb2f3b88aa0be4881dd3cdc251","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2018.10.006","type":"string"},"datatype":"url"},"type":"statement","id":"Q2333314$52BC2CC7-7CA4-4C18-9D12-6C6CBB161604","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"25d4acc2db6b0f35143b88da545d610cc58bcd03","datavalue":{"value":"W2899390563","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333314$68E64DBE-E5CE-4AAC-B551-56B3ACCD2695","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"787e8787fc0800d23d78fddfd9bf35254e758553","datavalue":{"value":{"entity-type":"item","numeric-id":801050,"id":"Q801050"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333314$061C4E5E-40A8-44B8-9A43-BF649EC46BFC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fcfdc5d6158991f32af2cf5057f70743de7ebb00","datavalue":{"value":{"entity-type":"item","numeric-id":1744410,"id":"Q1744410"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333314$D62E852D-4639-41B5-B119-F7C99BD7A38D","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":"Q2333314$7BD700F2-9B14-4EF7-B186-553F508CA92A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c193b2b170f7626fc739837cea7c223c4266fe6c","datavalue":{"value":{"entity-type":"item","numeric-id":853738,"id":"Q853738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333314$7FB746F8-1201-40FD-A400-0ED2B68D85B7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"47b8c3a63f5113f0209622b58f18640a08a06fa7","datavalue":{"value":{"entity-type":"item","numeric-id":1887151,"id":"Q1887151"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333314$9A48AE38-DEA5-4A23-9D6F-4D0E81430B37","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1851616a00610aaeabd4291b4d22573878184fd4","datavalue":{"value":{"entity-type":"item","numeric-id":3546313,"id":"Q3546313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333314$60EF63CA-C928-46DA-8A7C-0525E5E84A2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c382f571059f65c71d7c5267e06c23fa2d98eb72","datavalue":{"value":{"entity-type":"item","numeric-id":5917605,"id":"Q5917605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2333314$3E2B6A06-B568-4D9E-B28C-A86830B708DF","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"3668cb4695f978de6a02a11cff14a409a9fce53c","datavalue":{"value":"10.1016/J.ENTCS.2018.10.006","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2333314$D5127EA3-0E79-44D3-968E-8584B72CA281","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6cc5398b6df03581d13840f4c2ed624403400625","datavalue":{"value":{"entity-type":"item","numeric-id":2358702,"id":"Q2358702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0f78880316f0edaf7a4354e573aaa188ae40feb3","datavalue":{"value":{"amount":"+0.8323706388473511","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":"Q2333314$8EDB77BE-D85A-4D5C-92BD-05CAE62DDABC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"005232520771134680058c7ddbb399f79fb1a12f","datavalue":{"value":{"entity-type":"item","numeric-id":4647561,"id":"Q4647561"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b05f83b3bbd87f738a5bd07cc32d511254d51464","datavalue":{"value":{"amount":"+0.8081992268562317","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":"Q2333314$9561DE3B-D8D8-4383-AB22-6267255EDAA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a81bce5a2e732ce4597f77ee4cd8a8ee5be58f7a","datavalue":{"value":{"entity-type":"item","numeric-id":1595924,"id":"Q1595924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"917a9e448d7e908ef9535e863a12338dfa8953bb","datavalue":{"value":{"amount":"+0.8053510189056396","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":"Q2333314$72CEC039-D733-4C4D-9F2C-DB6AE4378581","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"dc20c0392397f580a2d4ce740056210eca74cccf","datavalue":{"value":{"entity-type":"item","numeric-id":3000279,"id":"Q3000279"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e5172db26189ce71152999724c9f125dce7ee325","datavalue":{"value":{"amount":"+0.8048843145370483","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":"Q2333314$FE9C7599-B19E-41B0-A18C-3C3D7C8E7F2D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"27d95eb8d46df09e1d483cb4bfe8c153b2222895","datavalue":{"value":{"entity-type":"item","numeric-id":2778886,"id":"Q2778886"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96a3b1dacea36809babae243c053c102f4399528","datavalue":{"value":{"amount":"+0.8036118745803833","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":"Q2333314$58A00849-51DE-4DF4-8170-7291F2785D30","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory","badges":[]}}}}}