{"entities":{"Q7361691":{"pageid":31520612,"ns":120,"title":"Item:Q7361691","lastrevid":105367271,"modified":"2026-10-07T13:36:46Z","type":"item","id":"Q7361691","labels":{"en":{"language":"en","value":"A Generic Framework for Verified Compilers"}},"descriptions":{"en":{"language":"en","value":"AFP entry VeriComp"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"877430007fd537c1d06fc6499a05d8e395f64fd1","datavalue":{"value":"https://isa-afp.org/entries/VeriComp.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361691$B03A7975-968E-41D0-B7A6-D23FCF96E600","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"c81b0ff7a16cf5dd5907466303464ced8542d6d2","datavalue":{"value":{"time":"+2020-02-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":"Q7361691$139CBED8-685B-4D1C-B0A8-97D5F13C34DE","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"e5724ef8b4ec23cf8c7c0feafb67eeb84d745382","datavalue":{"value":"Martin Desharnais-Sch\u00e4fer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361691$F7EE2303-E5D7-4A40-AF9F-3AC964CC9FBD","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"af54083f005d1a5b26789f904510ea1ab6d296ab","datavalue":{"value":{"text":"A Generic Framework for Verified Compilers","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361691$D6FB30E7-DA5E-4D07-ADF7-C474A552B2F5","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"440f855cb039fc6a31cd11294bda0dc665f06ad7","datavalue":{"value":"This is a generic framework for formalizing compiler transformations. It leverages Isabelle/HOL\u2019s locales to abstract over concrete languages and transformations. It states common definitions for language semantics, program behaviours, forward and backward simulations, and compilers. We provide generic operations, such as simulation and compiler composition, and prove general (partial) correctness theorems, resulting in reusable proof components.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361691$C7603D10-79D8-40F3-99A6-35C689E2F955","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":"Q7361691$AA30A720-FE72-4D9A-920A-B1F113B1EA10","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":"Q7361691$7C6BDFA6-CDEC-4507-BF45-7557BE313629","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":"Q7361691$00F9104B-BDC1-4C38-88D4-77C98C49E570","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A Generic Framework for Verified Compilers","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_Generic_Framework_for_Verified_Compilers"}}}}}