{"entities":{"Q7361752":{"pageid":31520795,"ns":120,"title":"Item:Q7361752","lastrevid":105368822,"modified":"2026-10-07T13:37:39Z","type":"item","id":"Q7361752","labels":{"en":{"language":"en","value":"Dictionary Construction"}},"descriptions":{"en":{"language":"en","value":"AFP entry Dict_Construction"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"7215445a21a49677e7a0e6917d2cbc1e0e8d4b92","datavalue":{"value":"https://isa-afp.org/entries/Dict_Construction.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361752$3F38FCB1-9E10-49A9-8277-A2684FA5CFEB","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"bb39e4a0c00eacb8782641ee71ab305789d63b9c","datavalue":{"value":{"time":"+2017-05-24T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361752$EA1F979E-CDE9-4E88-81E5-907C98897C85","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"bf5d485796582ea615cfd5e7c0148e1add1641d3","datavalue":{"value":"Lars Hupel","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361752$E24B0786-8AA3-498B-9CF9-53918DD5CB81","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"055bb828dab60e528fe9f4711035f3397cc1e626","datavalue":{"value":{"text":"Dictionary Construction","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361752$2D420F6C-9E63-44BF-A88F-07C2DCE23181","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5f24589faa5ab0ba6cb9dbe55600ff7a3e21face","datavalue":{"value":"Isabelle's code generator natively supports type classes. For targets that do not have language support for classes and instances, it performs the well-known dictionary translation, as described by Haftmann and Nipkow. This translation happens outside the logic, i.e., there is no guarantee that it is correct, besides the pen-and-paper proof. This work implements a certified dictionary translation that produces new class-free constants and derives equality theorems.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361752$5F0AC615-4E76-4BBE-A910-DDCD9E4CECF6","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"14533123e0b9e73c06f9737a070ee002c25f5f1b","datavalue":{"value":{"entity-type":"item","numeric-id":3612442,"id":"Q3612442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361752$B7ED9F66-43AD-42B6-846C-AAD527C1C36D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"931c42c28f22f89fe1b66164f9ececc2021ac1a2","datavalue":{"value":{"entity-type":"item","numeric-id":3558332,"id":"Q3558332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361752$53FB696E-5741-48A1-B2AF-46835A4E878E","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":"Q7361752$E380C276-8F1C-4FE3-BA3D-B6A00F613B0C","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"27e971e25f48a406ca09caf18a9e463d40cb63ef","datavalue":{"value":{"entity-type":"item","numeric-id":7361166,"id":"Q7361166"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361752$98EC5EF5-D00C-4F5D-8E22-5CD21D701429","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"fe831ba54f2ce413cdc81454989524ac1bf63b6a","datavalue":{"value":{"entity-type":"item","numeric-id":7361149,"id":"Q7361149"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361752$797F378F-4308-4A16-84E9-BAC62D2AF9C3","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":"Q7361752$F96A3FFA-0F51-4410-99B5-3DBBC41C3C9C","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"7a918ca57cbef7417c708001c9499e7e295238c0","datavalue":{"value":{"entity-type":"item","numeric-id":7360836,"id":"Q7360836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361752$6B0F94E2-4B23-4C9D-9744-33D3A54647DF","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":"Q7361752$17EBF257-0C9F-4D31-AFB6-C1A8DF3FE713","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Dictionary Construction (AFP entry Dict Construction)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Dictionary_Construction_(AFP_entry_Dict_Construction)"}}}}}