{"entities":{"Q2871835":{"pageid":2882555,"ns":120,"title":"Item:Q2871835","lastrevid":79529843,"modified":"2026-05-06T14:07:45Z","type":"item","id":"Q2871835","labels":{"en":{"language":"en","value":"Normalization for the simply-typed lambda-calculus in Twelf"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6244365"}},"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":"Q2871835$F181BFD5-A5FE-48CA-8639-F47F755DC90C","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"d51e679f80a087da0343de4e7d7df5ec3039a06e","datavalue":{"value":"1278.68245","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871835$BE2B7412-0ED8-4A94-8423-5FF006EB907E","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"9fd295c773add0c694cee3f65e8e7cf93dc4bc27","datavalue":{"value":{"entity-type":"item","numeric-id":923882,"id":"Q923882"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$783511D4-120B-4EFD-9846-B1DBC00C804D","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$6D75690E-92B7-4023-A035-0B2513E994DF","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2c704b287c68a3d4d8361a025642d6eba13574eb","datavalue":{"value":{"time":"+2014-01-10T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2871835$4BF607DB-2E62-4D61-8DE2-E7AD1185D70B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871835$48259B72-A92B-49A0-BCA7-890266046604","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"25aa969dcca62ee94c95b2a54e4102ee8a17d130","datavalue":{"value":"03B40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871835$EAEF6AFF-F9B4-4217-A195-A5AEB127D508","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"ef863b72448df4b73016b02d66ac48843ce21a23","datavalue":{"value":"6244365","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871835$E3334877-097E-463B-87C8-58A68DEDBDAE","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ba03543f6eb8246f3663782c06e96c302c8beacb","datavalue":{"value":"Edinburgh logical framework","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871835$0BFAF5C9-4666-43E1-9591-12C08857B106","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6610928532c28e5c20988bf9f6bbde45ae859367","datavalue":{"value":"HOAS","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871835$DE333E19-EC79-4340-B33D-C5DB083AC958","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5ed5b36acbbcdd78ff381b3635ec25a20340482b","datavalue":{"value":"mechanized proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871835$3DD10257-8835-4375-B5D3-9C09BD29E763","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"4296281254337308ad2c5f734043898466afdb58","datavalue":{"value":"normalization","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871835$FE5D30CE-7726-40E6-8B18-837D410F861E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8a7faf2d5c8d76731eb2c0fa9732494500b1c909","datavalue":{"value":"Twelf","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871835$3DE9A59F-CEA6-4EB5-98A3-FAE2E0DCB218","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$03F50E34-CEAE-48AC-94D0-6D438811688E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"55d1796d289926821ff098bc5ea53615142e836d","datavalue":{"value":{"entity-type":"item","numeric-id":21664,"id":"Q21664"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$23302FB4-B522-4D8B-B3D9-8561687E8C4D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"040fe209bf9959da562393c0e37eb31592733af3","datavalue":{"value":{"entity-type":"item","numeric-id":18957,"id":"Q18957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$507338A6-4F09-486B-BA7E-5489E90D09BF","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":"Q2871835$6203AD56-D057-4164-B0AE-89F3B6D4E9E2","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"880f511544dec730da214ce916b2aa41fc81ddb8","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2007.11.009","type":"string"},"datatype":"url"},"type":"statement","id":"Q2871835$FECC62E6-B62E-46D5-98B7-9336EC82581C","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"07488cda905de0176b754f86f3df3ad134f4b5b2","datavalue":{"value":"W2152365225","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871835$C93776DB-8E55-4427-A7F7-447CD599DCF5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d8bfe191ca90d3395347096033dd0a0643030e0","datavalue":{"value":{"entity-type":"item","numeric-id":4281462,"id":"Q4281462"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$DFD4123F-5119-48E4-B9A6-271CFAB63C1D","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":"Q2871835$586D844E-3029-4D71-8EED-E2D49D4CEFA2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"203af7b2224e70d9229da9b044eb4282ff6c7420","datavalue":{"value":{"entity-type":"item","numeric-id":3024835,"id":"Q3024835"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$5DC0D2D0-6DBF-43B1-BF30-D3ECE22DCA17","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"021e6e2184fd3d7f831680d56b426b95217eac7a","datavalue":{"value":{"entity-type":"item","numeric-id":4033837,"id":"Q4033837"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$E504999D-69B7-4883-A24C-B7EEDD670950","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0c3c69fa2672b8fa81e2d2be45ac3f1049ef642d","datavalue":{"value":{"entity-type":"item","numeric-id":5277716,"id":"Q5277716"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$97DFA416-28FD-48F7-A6F2-04BD048AEF13","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":"Q2871835$A7A4BB52-D46A-4B4E-A2FB-0321EFF1EC70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6063e4a144bafe1447ae8b10555347d26c418f1d","datavalue":{"value":{"entity-type":"item","numeric-id":3189797,"id":"Q3189797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$B33BFD81-C34E-4873-B391-D420035FF9B3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8a4d4048d68302ad95851d7b1bf999b446bba869","datavalue":{"value":{"entity-type":"item","numeric-id":2751369,"id":"Q2751369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$0E514776-A97D-4771-93AA-E21B365FDD5B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b144c0c520c17509ac5daded8f5ecbc80c815e60","datavalue":{"value":{"entity-type":"item","numeric-id":4539625,"id":"Q4539625"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$933F01B5-745F-4952-B25F-E9483EA2E6E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"be8cf2dc492019f717e5e3e0a386be0e43cff24e","datavalue":{"value":{"entity-type":"item","numeric-id":3559763,"id":"Q3559763"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$397A1849-36D6-4131-8C4B-681A43C70FF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e6a84ea93cf6a73175ac30cdbefbac22005aa8d","datavalue":{"value":{"entity-type":"item","numeric-id":4323124,"id":"Q4323124"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$40EB3987-FE75-4DAF-8258-ACC823A5A6A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db9d1ac17655f7d23b5941696fc397faeec07acf","datavalue":{"value":{"entity-type":"item","numeric-id":1286373,"id":"Q1286373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$B68E4750-2117-4939-BEFA-99F0F66DB602","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa19d45127427927ec930c6ce8f8170b9db93184","datavalue":{"value":{"entity-type":"item","numeric-id":5712317,"id":"Q5712317"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871835$E23F3C2D-36B9-4301-A0CF-E85D6BEB5BE2","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"19b227735a05e80287ca99a8a8d81138a0c4c70c","datavalue":{"value":"10.1016/J.ENTCS.2007.11.009","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871835$33814905-2F1F-435A-94AA-AB0120A9C09F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7982a19266fc56d5fc7f47e93f166157e2f0819b","datavalue":{"value":{"text":"Normalization for the simply-typed lambda-calculus in Twelf","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2871835$84C28BC8-4A52-4BDA-9D49-F77544F6FF23","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":"1ef58689cdc9b1b2c35873b61b674e4d454e1fdc","datavalue":{"value":{"amount":"+0.8369261622428894","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":"Q2871835$00BBEBCF-4C0B-42A1-A637-F2A60B0BA94C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"13ddc27e400e1d79f8de31cb38a2e81546e0a52a","datavalue":{"value":{"entity-type":"item","numeric-id":4946629,"id":"Q4946629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a1eea68a9f903f0970d90e8ae54e041e4d314b16","datavalue":{"value":{"amount":"+0.8125752210617065","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":"Q2871835$0A448003-5D8A-4189-9F5A-A07F50E7AC98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f65ccfe89edfee7e808370feea971f6c76e59d31","datavalue":{"value":{"entity-type":"item","numeric-id":5898172,"id":"Q5898172"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4dc16f51138769db01ce6815f026aedcfae39600","datavalue":{"value":{"amount":"+0.8018843531608582","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":"Q2871835$238F8F2E-D8C7-4E92-8604-C8292A7CDD4F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a11a1210fbc388975d2c306dcac20ebc18d71c5a","datavalue":{"value":{"entity-type":"item","numeric-id":817701,"id":"Q817701"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"27f4b88a36022322afa6e5b4b2d85a22337b0ebc","datavalue":{"value":{"amount":"+0.7997704148292542","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":"Q2871835$7618300C-D23E-454D-A128-893FB55CAF12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"42797fc209eaaddb74c3306a25952bf259efdce8","datavalue":{"value":{"entity-type":"item","numeric-id":1850959,"id":"Q1850959"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4da9eab41e1ccd3aebef01ec02694d6558e3a8d9","datavalue":{"value":{"amount":"+0.7955964207649231","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":"Q2871835$71361F1E-F057-4D21-9A4E-325483793E8D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Normalization for the simply-typed lambda-calculus in Twelf","badges":[]}}}}}