{"entities":{"Q51730":{"pageid":51786,"ns":120,"title":"Item:Q51730","lastrevid":105426701,"modified":"2026-10-09T10:06:00Z","type":"item","id":"Q51730","labels":{"en":{"language":"en","value":"CakeML_Codegen"}},"descriptions":{"en":{"language":"en","value":"AFP entry CakeML_Codegen"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"bd30f900aba6962e744e50b9da55e47ebf9e3df4","datavalue":{"value":"36028","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q51730$E8A3A82D-A121-4B1B-BEAF-3EDAF56BD8D4","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":"Q51730$9DA4C806-4385-4554-9228-B2DACE4DA740","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"27cc68c25d0c098a1a101f347e2e26ea061b8bb0","datavalue":{"value":"https://www.isa-afp.org/entries/CakeML_Codegen.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q51730$1C16B08C-51C0-41A8-91C7-E0F7EF2EE63C","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q51730$EDC7EE02-C1F0-4C4B-9D15-0435A055E947","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"47548059e3416b4b47c737ba6e24ccdeda7d9657","datavalue":{"value":{"entity-type":"item","numeric-id":40548,"id":"Q40548"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$574C35A1-C052-48D2-895B-6CF44E135500","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$519DEB80-76D9-4F09-A272-B75CBC5238DE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$A3B6BFBB-D6A3-4E84-90A5-8B992A3F10A0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"0470ff816111d0af07246978dfc3d7a51d0e39f7","datavalue":{"value":{"entity-type":"item","numeric-id":51731,"id":"Q51731"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$5E30F3A8-811A-4A4F-B825-B4F2CDA8F74B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4a5d7cc7c93c22bf9c8fa550419d7f2b201a4c87","datavalue":{"value":{"entity-type":"item","numeric-id":31827,"id":"Q31827"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$1D4CCAA7-B454-415C-9022-097902BD27CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7343f563fd02ee3f7d39ccb038f5c1c6c726769a","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$EBB3636D-82B9-4CB0-9A80-AFB427FB23C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a2a767ccd0e9bdc5b1b4a2069a6679f9340a857a","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$CAB22ED4-604B-46D0-AC22-93150D2292E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$0EC3295F-06C8-4EF3-B544-657A116DC86F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$68D488DD-9811-47CD-A239-5D6768C7E997","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"139c69b2a23f419923a7989e28183ef8179b6836","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$D708DC36-1B5C-4F42-AAEA-5A8716384159","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"31654f1fbd1ffa202d15bd7137d6c443745637b9","datavalue":{"value":"https://isa-afp.org/entries/CakeML_Codegen.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q51730$EF9ACA65-5688-493B-B3E6-0F244F851C33","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"bf5d485796582ea615cfd5e7c0148e1add1641d3","datavalue":{"value":"Lars Hupel","type":"string"},"datatype":"string"},"type":"statement","id":"Q51730$126D17EF-7BB0-419B-B08B-F5616721BB02","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"4ad7a8791a881fd0065e1a94a121f1442d019a2d","datavalue":{"value":"This entry contains the formalization that accompanies my PhD thesis (see https://lars.hupel.info/research/codegen/). I develop a verified compilation toolchain from executable specifications in Isabelle/HOL to CakeML abstract syntax trees. This improves over the state-of-the-art in Isabelle by providing a trustworthy procedure for code generation.","type":"string"},"datatype":"string"},"type":"statement","id":"Q51730$11C5655D-1B7D-4B67-A4FE-776397DCDDB7","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"b5764d15c9b3cde4d0f06357ae8f3151e37264b7","datavalue":{"value":{"entity-type":"item","numeric-id":7361198,"id":"Q7361198"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$08C55FC1-1507-4C43-9A82-2F75E0E69357","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"4c4a1fb1b4b4d3c440cc14dfae980ce61cdb0f8d","datavalue":{"value":{"entity-type":"item","numeric-id":7361455,"id":"Q7361455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$42F7002F-9D44-4E49-BC68-77983C38A765","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"3f3e10892342ae666467aa53aae82b3dd6119a57","datavalue":{"value":{"entity-type":"item","numeric-id":7361752,"id":"Q7361752"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$17D444F0-32AA-4272-8E99-310ECBD75BDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"27b52b6cd3774fbcb9d039f540c090ccbcb48bbe","datavalue":{"value":{"entity-type":"item","numeric-id":7361834,"id":"Q7361834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$B1391104-7783-4C66-89E6-85CE251CAD25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"53010cc24962861c2adfe9ea878f0281f084e7d6","datavalue":{"value":{"entity-type":"item","numeric-id":7361921,"id":"Q7361921"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$33AEB920-9DA3-4843-9918-8345383C116E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"693b52a7b9dd01d1026b7fe332818dab80c9c06b","datavalue":{"value":{"entity-type":"item","numeric-id":7361590,"id":"Q7361590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$76654619-8898-4EE9-9590-92F5DC7EA704","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c19d3d2985ae4c7264c7edf9445a6e4552a316dc","datavalue":{"value":{"entity-type":"item","numeric-id":7361880,"id":"Q7361880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$DFC44E69-F8FF-475D-AADA-D7AB348816EE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"c8b055357156b513ebffa05abff4ab0fc053c1d6","datavalue":{"value":{"entity-type":"item","numeric-id":7361662,"id":"Q7361662"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q51730$B64F2770-A968-4B65-BE0A-561EFE358DDE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"95484946e883fc7b4dd3685da23c3ff319dc5c53","datavalue":{"value":{"time":"+2019-07-08T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q51730$AD4CD2B3-13D3-4120-A74E-CA28AB24ECB2","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"10fa82ee06a2f9494f2107b149c71a384292b368","datavalue":{"value":{"text":"A Verified Code Generator from Isabelle/HOL to CakeML","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q51730$E20A0FCA-FDDB-44B7-B84B-6445928475A0","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":"Q51730$5EDBD995-8FC2-448A-A5B9-746579128848","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":"Q51730$8E51038E-1FA2-482F-AFCD-8E46DD28CF0A","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"CakeML Codegen","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/CakeML_Codegen"}}}}}