{"entities":{"Q2871863":{"pageid":2882583,"ns":120,"title":"Item:Q2871863","lastrevid":79530095,"modified":"2026-05-06T14:07:47Z","type":"item","id":"Q2871863","labels":{"en":{"language":"en","value":"A list-machine benchmark for mechanized metatheory (extended abstract)"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6244438"}},"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":"Q2871863$9161F92F-7654-4A63-B936-A9A0F1FEB031","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"dd28a3bf492c36c47a77bfb8a0e8f414350f12e7","datavalue":{"value":"1278.68247","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871863$F0498693-C883-4DED-9712-59629F9BE3ED","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"fc26ae99955b17096664472ad434caf6f770734f","datavalue":{"value":{"entity-type":"item","numeric-id":1663237,"id":"Q1663237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871863$046E12D0-6E6E-4FFB-B326-A7A7579B38DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c4b1e35c1c4bff0a8e8e775e8600e2e952b118ae","datavalue":{"value":{"entity-type":"item","numeric-id":848738,"id":"Q848738"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2871863$23774B7C-4AA1-4072-B39D-DF55012CEEFF","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":"Q2871863$86C012F3-B1B9-4854-A17F-4A9916DA8393","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e49c9adc5917ebd4385aebd9ba9852874a136e65","datavalue":{"value":"http://www.sciencedirect.com/science/article/pii/S1571066107002344?np=y","type":"string"},"datatype":"url"},"type":"statement","id":"Q2871863$CAD0283F-7F0E-4725-8F8F-29D7FB7B9DB1","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871863$3B24E45C-9137-443F-9F75-051A90BF17FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"f3affb2aa66be15f2a63c60d2aaa92bd143e6d46","datavalue":{"value":"68N20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871863$795E97DA-B54A-418B-AA5C-B2C5DEDF66CA","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d6386aa29015ccaa9088a7dadca08331f1b2782d","datavalue":{"value":"6244438","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2871863$562F3522-1792-4870-973A-BEBBEAD2199D","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"22498cf86e242a38d9fe355523225aa55193233b","datavalue":{"value":"theorem proving","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871863$BA31131C-800C-436C-921D-6B1DDEF93A61","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ddbcb2073b5c7b755f2e5b673e59622629e687d7","datavalue":{"value":"proof assistants","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871863$BAC4A007-EDBA-454C-BAA0-35A20F72C573","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"df198e9539af8ee1221a27fc303d184b5cc81a2c","datavalue":{"value":"program proof","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871863$111245F7-09D5-43E2-BB3A-EC269D26DD3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"acd9c52c59d07d5822d39f1d47e4205b4637b9d3","datavalue":{"value":"compiler verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871863$2407D39B-10CB-48D7-923B-F5F2DBDA5B72","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3f310826d02e1242e24d99b67e4a216f73851f5c","datavalue":{"value":"typed machine language","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871863$7ABFE32C-1981-4937-A374-24CCEB730196","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c3a6e871a284af917cfc8de81b27bddc18a2460a","datavalue":{"value":"metatheory","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871863$E566E23E-92C4-43F8-8175-69A5C74815AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"09e5b68927baf737cf4d5adadb4664c931aae1c2","datavalue":{"value":"Coq","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871863$1E8DA475-3C29-4FAF-B99F-4B878E237AF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8a7faf2d5c8d76731eb2c0fa9732494500b1c909","datavalue":{"value":"Twelf","type":"string"},"datatype":"string"},"type":"statement","id":"Q2871863$0FB6A179-A0A8-4F82-9F6B-1936BF0B82D5","rank":"normal"}],"P1463":[{"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":"Q2871863$FF399E38-0DA0-4F56-AC73-FD7A1339CFA0","rank":"normal"},{"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":"Q2871863$FA1986FB-E03D-420C-A64F-470D4E7848CE","rank":"normal"},{"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":"Q2871863$523592F7-9F85-462C-A110-93C46DEF93EB","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":"Q2871863$62F3B5C8-F10D-49B2-89D9-41991EF7670E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b2fc77492e9f46ee0ad383919bec7a4d292db5d2","datavalue":{"value":{"text":"A list-machine benchmark for mechanized metatheory (extended abstract)","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2871863$6B9A59B5-D42F-4C87-9ABC-0F94C29B08DD","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"379e0292ca3acb9bd4c247f3239b0373dd09f4da","datavalue":{"value":{"entity-type":"item","numeric-id":1945921,"id":"Q1945921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"716654ce7da1f22b9b7a4b443ef184420efc6771","datavalue":{"value":{"amount":"+0.9949397444725036","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":"Q2871863$ECE0EF7A-DBB5-4B85-AB7A-3A1090B9D80E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e3a108876ee2d73cf53e48814576175e292747f","datavalue":{"value":{"entity-type":"item","numeric-id":5110924,"id":"Q5110924"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a671702be8f24211406f449897d57f9ccdcf545","datavalue":{"value":{"amount":"+0.7509127855300903","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":"Q2871863$9BD410E8-EE82-4E72-A41B-EC884FD39D15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"51b15cbe5ea309bdc48ff40b9c5acde598f0666f","datavalue":{"value":{"entity-type":"item","numeric-id":5477646,"id":"Q5477646"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c73ab748655973420bde3205bf0f123d7102642","datavalue":{"value":{"amount":"+0.7460435032844543","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":"Q2871863$2B350D07-4766-41FB-B05D-CDF5225F3596","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"753995a7591fdc07125446e04545c9e631973be2","datavalue":{"value":{"entity-type":"item","numeric-id":4474853,"id":"Q4474853"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4be6f4fa7bc1d1cdc8c4080dd157256f89fe1fc8","datavalue":{"value":{"amount":"+0.7178360223770142","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":"Q2871863$BDB25C90-07DB-45A1-9BAD-D9BFC8187A67","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2830883c821c59e8ea357fc4abf509bdbccc9c9e","datavalue":{"value":{"entity-type":"item","numeric-id":1945919,"id":"Q1945919"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"96c18ff86902f95933b0f70c31177f849c06af1f","datavalue":{"value":{"amount":"+0.7137326002120972","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":"Q2871863$5F0C0861-E806-47F5-B33B-852A807F2E47","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A list-machine benchmark for mechanized metatheory (extended abstract)","badges":[]}}}}}