{"entities":{"Q7361317":{"pageid":31519490,"ns":120,"title":"Item:Q7361317","lastrevid":105364853,"modified":"2026-10-07T13:35:30Z","type":"item","id":"Q7361317","labels":{"en":{"language":"en","value":"Normalization by Evaluation"}},"descriptions":{"en":{"language":"en","value":"AFP entry NormByEval"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9b48979037b0bd56a2580a2ffd99c29ca5ec3447","datavalue":{"value":"https://isa-afp.org/entries/NormByEval.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361317$C746693E-1251-4CDE-BFAA-AE2F3234AFEA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"118eb39459fbba91acbfa1c46ee7e29cd76ebdf5","datavalue":{"value":{"time":"+2008-02-18T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361317$194222F5-756A-4E4B-9160-54D8F6E79026","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"1d3422397d6b76cc523bfaa4501d90de313ec122","datavalue":{"value":"Klaus Aehlig","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361317$D09EC9F9-C761-4FEF-B9A2-BEF3308F8E83","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"78083bbf5b06a4f292e9e00ee445948e4fa51db5","datavalue":{"value":"Tobias Nipkow","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361317$ADDA744C-5EBC-4F59-9709-4C0D2F0A7DED","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"cc9d99ddfa37fa343b19e965140e5665c821d9df","datavalue":{"value":{"text":"Normalization by Evaluation","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361317$BAB4E8EA-5E8A-4A25-AB5F-E6F9B449692B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"15507f530adee9f1fbb5ab16ed62433247f4a189","datavalue":{"value":"This article formalizes normalization by evaluation as implemented in Isabelle. Lambda calculus plus term rewriting is compiled into a functional program with pattern matching. It is proved that the result of a successful evaluation is a) correct, i.e. equivalent to the input, and b) in normal form.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361317$8AEB7739-39EF-4D90-80A0-A3DCE61F385F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8456e5ce61ce50df853e86b502252b5c44643be8","datavalue":{"value":{"entity-type":"item","numeric-id":3543648,"id":"Q3543648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361317$3568B116-B1EA-4530-9F5E-E89011999203","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361317$CC53556C-7D1D-4825-9546-588DF83B36A0","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"05d95abb47cad8232a89a6f87120d0cbd9525961","datavalue":{"value":{"entity-type":"item","numeric-id":7360794,"id":"Q7360794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361317$43828126-EF9B-4C2F-A0D0-872428113F29","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361317$1210AEB7-2433-4D36-9BE4-75D5A4152DA5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Normalization by Evaluation","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Normalization_by_Evaluation"}}}}}