{"entities":{"Q2229159":{"pageid":2239902,"ns":120,"title":"Item:Q2229159","lastrevid":53940203,"modified":"2026-01-25T23:25:08Z","type":"item","id":"Q2229159","labels":{"en":{"language":"en","value":"Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7313971"}},"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":"Q2229159$02D385CE-9466-4252-A286-4F542E904162","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"1010767eeb0704110a2f09e15a13465affd3ec4f","datavalue":{"value":{"text":"Strong normalization for the simply-typed lambda calculus in constructive type theory using Agda","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2229159$B0514ED0-148C-4B0D-842E-CD316713B64C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"1221beba3139cf85775b76f87fc32b34b640fdbc","datavalue":{"value":"1498.03044","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2229159$6DE661E7-F88B-4E06-8188-E4F249796D0D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5fd8de591c266df6994095a1dd9ed78e443d9a11","datavalue":{"value":{"entity-type":"item","numeric-id":2229158,"id":"Q2229158"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2229159$F50E27FA-DED8-4874-82E8-88E890D6DB9C","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":"Q2229159$D70B0136-38A8-4E8C-B374-6FCCA69BB294","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":"Q2229159$894FE97A-2E91-4698-A4E8-F33095D134B3","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bf0749869f595759ee793dee0f3189be235834d4","datavalue":{"value":{"time":"+2021-02-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2229159$F7109CF2-1D84-49C5-A3E1-B62DAEDE5E06","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2229159$6970F14E-B2EF-43FB-AE93-27CBEDDE0F3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"beee3648fc78215bd3297256b1ada8fd8f08734e","datavalue":{"value":"03F05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2229159$EC0A2F02-6E70-4DBA-BEBD-CE91AF0CB663","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"9d16bc3e9081106e8c0a3815e02fbf34868a61d2","datavalue":{"value":"7313971","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2229159$52DC8904-268C-4FE6-AEA8-2950C037BD14","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"34ae3a8d9f3401a083509ec6ab2b6f0f2deb2a29","datavalue":{"value":"formal metatheory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2229159$1ABF89E3-FBC2-4C3D-9D68-5E748731C28D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5b876698d821b50cd7ba02ddb5424ed80f1905d8","datavalue":{"value":"lambda calculus","type":"string"},"datatype":"string"},"type":"statement","id":"Q2229159$C5075C5A-288B-4D40-9A39-D1856B2ECB96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d6c658f92cfca10399e0b9df9aa408c3bc22cae6","datavalue":{"value":"constructive type theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2229159$F860A6EA-2AA6-4850-AC64-2E9B4ADA80D6","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8be5ee5254d2a781e0ec7bc0b35265c3f1813a9a","datavalue":{"value":{"entity-type":"item","numeric-id":22078,"id":"Q22078"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2229159$57182CCE-D8B9-44ED-A493-A996D9EB2840","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d40b61763c81cd80c5c82e03c39b2fdb5cbb80a2","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2229159$BC1DE31F-B600-4E16-AA6F-F0C6E8A11986","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":"Q2229159$AF9D6D47-BC12-4B5D-A054-1769EA06F15B","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"5f2a6723d1a56cf0098d1e5841646230333c61cf","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2020.08.010","type":"string"},"datatype":"url"},"type":"statement","id":"Q2229159$CD8E3DA5-9580-485F-84B8-D4810FEEED6A","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"3596985ec60b6ddf5ec46c5f540aa565834d2df9","datavalue":{"value":"W3093261255","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2229159$407548CB-25B1-4223-8A26-03345E8BD877","rank":"normal"}],"P12":[{"mainsnak":{"snaktype":"value","property":"P12","hash":"f0947102ac94df6cd3ee67ed4dfdf4267d788682","datavalue":{"value":"Q113317312","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2229159$9268E900-670F-4D4E-8A23-331B8A6CCF9A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4cb7bc6676bcf4ae8d66c7a793e7ffdddba9905","datavalue":{"value":{"entity-type":"item","numeric-id":5110924,"id":"Q5110924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2229159$8B9B260D-8C9F-4D8B-8847-96FE6B206391","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18b5ba4e3d1bf82f550bf1c7b244d01dbead3656","datavalue":{"value":{"entity-type":"item","numeric-id":2358702,"id":"Q2358702"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2229159$505FEA35-FA65-4E94-9063-279075C83E81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc1c245995c89f282e75c9bdf34b76dfef951a2","datavalue":{"value":{"entity-type":"item","numeric-id":2333314,"id":"Q2333314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2229159$334B7667-6357-4B19-A2CC-0D8E3C2EFCAB","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":"Q2229159$6E98A299-663D-4608-BE39-21103FB4DAEB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4ccc272df6e3f638456d722d8f630056eceb056f","datavalue":{"value":{"entity-type":"item","numeric-id":5565113,"id":"Q5565113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2229159$B304A03C-4820-4834-A6BB-1821A8BD80DC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fe478b1c9e3755ecb4683bf76c070eb4413865c0","datavalue":{"value":{"entity-type":"item","numeric-id":1407578,"id":"Q1407578"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2229159$59C68D88-FB44-410D-9AD2-011BF3F26078","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a5f149ec444851c81f8f28cc669b90ac06bcf6ea","datavalue":{"value":{"entity-type":"item","numeric-id":1106190,"id":"Q1106190"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2229159$6A723779-83B8-4DC6-A129-4888CA61018C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4f8f6dff394ac274489a2a8165abb84f760b4be","datavalue":{"value":{"entity-type":"item","numeric-id":5394605,"id":"Q5394605"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2229159$BA47D82D-48F9-4120-9100-A1EE4754FFCC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ead74ef3f97b72bc673b8aaa224e07d01a3354a3","datavalue":{"value":"10.1016/J.ENTCS.2020.08.010","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2229159$5FF1ACC2-4A1B-403F-8B14-E580A11B89FB","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe7e2cfcf9f8ac0233557b6d690d557c3ef22bc1","datavalue":{"value":{"entity-type":"item","numeric-id":2871864,"id":"Q2871864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4b5895aca960f400de2fb38679f4513866512cd4","datavalue":{"value":{"amount":"+0.8459888696670532","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":"Q2229159$ABDA673D-F5A5-42C2-870F-37EA783736E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"81687b63ee04b4d5b3d7408428fcafd50bae5c4b","datavalue":{"value":{"entity-type":"item","numeric-id":4281462,"id":"Q4281462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ba7119fa8ea3f844c3b2341493c8fa4a8efaeb71","datavalue":{"value":{"amount":"+0.8005547523498535","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":"Q2229159$D135E89E-8509-49E8-8450-B1E19E0CC48D","rank":"normal"},{"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":"ba7119fa8ea3f844c3b2341493c8fa4a8efaeb71","datavalue":{"value":{"amount":"+0.8005547523498535","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":"Q2229159$1B4A337C-BBEA-4DB2-B277-92F8540D6119","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"26a1e95e103b48b2ec9f98a8e4b8a2be4e2bde0b","datavalue":{"value":{"entity-type":"item","numeric-id":3599163,"id":"Q3599163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"596374094ae4e62cecbf227ff6aa59d426ba8c9f","datavalue":{"value":{"amount":"+0.800001323223114","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":"Q2229159$5A8C3D26-DE67-4DB5-9149-9AD48D06D8CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e9e0fc5f0014bdd6c8e8417e372280fe791b4099","datavalue":{"value":{"entity-type":"item","numeric-id":1891251,"id":"Q1891251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7c34669967c5b7cb3ea4bac915c4a46e841978a2","datavalue":{"value":{"amount":"+0.7964751720428467","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":"Q2229159$643FC705-B840-4318-98F2-5B18A8711B9D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2229159","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2229159"}}}}}