{"entities":{"Q40354":{"pageid":40410,"ns":120,"title":"Item:Q40354","lastrevid":105426332,"modified":"2026-10-09T10:05:11Z","type":"item","id":"Q40354","labels":{"en":{"language":"en","value":"Memoization"}},"descriptions":{"en":{"language":"en","value":"AFP entry Monad_Memo_DP"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"609a860daa4811f3d51045a7585b1a0d1fe29af8","datavalue":{"value":"28640","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40354$9D99C170-27A5-4E35-AF6B-8A4E129FF67D","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":"Q40354$DAEC2A10-56C2-4354-96EC-D75415144001","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"a8ca8f61343d556cfc7fe2ea3ac56020ace8e799","datavalue":{"value":"https://www.isa-afp.org/entries/Monad_Memo_DP.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40354$2259CC8D-538A-4C0A-B4AB-04F4765A6785","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40354$6E69F176-49EE-4FCE-8440-31818293BB1C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"541da1e359051dfcf3c498b9f1f1f8f905fbafe3","datavalue":{"value":"90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40354$25E76847-FAF6-48AB-9205-B6BFBB99F2CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a8aa801742e290b2e6820d89349e86d8f23555f","datavalue":{"value":"90.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40354$137E2617-1F85-48EA-BE86-23E99BF3909C","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"184599057b28a50637cabcc0548f7fee38f33c41","datavalue":{"value":{"entity-type":"item","numeric-id":40353,"id":"Q40353"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$A4377854-F1A7-4F80-875D-534E18ECDE1C","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":"Q40354$6DB550B3-2ED5-4211-B933-D778D5789044","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":"Q40354$771EB8FF-1CB5-4105-BF94-B9F59F9D9DDE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"a5257433611ab76f839d2dde4456f4ad35c212e5","datavalue":{"value":"https://isa-afp.org/entries/Monad_Memo_DP.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40354$7DEA01B9-5CED-4C9A-995A-99C1360C89CF","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"8ad3851178fd4351b5225d703448b2fe1218d392","datavalue":{"value":"Simon Wimmer","type":"string"},"datatype":"string"},"type":"statement","id":"Q40354$49795D6E-D187-4333-AA0D-B103099B812F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"13ea027972e16b525b8e67477a370187c840ce37","datavalue":{"value":"Shuwei Hu","type":"string"},"datatype":"string"},"type":"statement","id":"Q40354$AAD526C8-9369-4211-80E8-248142F768CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"78083bbf5b06a4f292e9e00ee445948e4fa51db5","datavalue":{"value":"Tobias Nipkow","type":"string"},"datatype":"string"},"type":"statement","id":"Q40354$D8F3BCD8-EBEC-4F4C-BBE8-D0B8DE963291","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"62937663a963ab421dc76d4b30b760391f09b016","datavalue":{"value":"We present a lightweight framework for the automatic verified (functional or imperative) memoization of recursive functions. Our tool can turn a pure Isabelle/HOL function definition into a monadified version in a state monad or the Imperative HOL heap monad, and prove a correspondence theorem. We provide a variety of memory implementations for the two types of monads. A number of simple techniques allow us to achieve bottom-up computation and space-efficient memoization. The framework\u2019s utility is demonstrated on a number of representative dynamic programming problems. A detailed description of our work can be found in the accompanying paper [2].","type":"string"},"datatype":"string"},"type":"statement","id":"Q40354$3CEBEE52-453F-4556-A5F5-A49D4BB60D06","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9c60f93a1843fcd9c0656971efa4327b435decb9","datavalue":{"value":{"entity-type":"item","numeric-id":4736387,"id":"Q4736387"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$2BE67518-4AF9-486D-8549-A1D8B7580F2C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"efb9fbef47df8e69c5d186f6867b4d645fc1d14a","datavalue":{"value":{"entity-type":"item","numeric-id":2351422,"id":"Q2351422"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$CFA46576-A709-4C11-A660-F454628C66C9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e264974062f53b439460b85662778a60b49509d","datavalue":{"value":{"entity-type":"item","numeric-id":2926333,"id":"Q2926333"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$100B908E-3499-479E-82F2-56341B223A92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4f6dbc9d14aa31bda7ad388a4db3885ef278ef66","datavalue":{"value":{"entity-type":"item","numeric-id":1791205,"id":"Q1791205"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$5511E0A2-5335-4CEA-826D-1F44E4589B82","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"da0d795517e293a55fbffeee6d84c637293c8bf8","datavalue":{"value":{"entity-type":"item","numeric-id":5327339,"id":"Q5327339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$70CCE1CA-FDED-40EA-A662-8A33631760F6","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":"Q40354$28CA5B07-3DD3-436A-A2DD-9D0D40067372","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b1758902a66e2332f9d1d0268ecf38eeeb4d377f","datavalue":{"value":{"entity-type":"item","numeric-id":3862379,"id":"Q3862379"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$48A76C06-4736-4E08-8035-DC0766CCE2C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5a1ce762817aa67ba84d34579fd3b9060a2c653","datavalue":{"value":{"entity-type":"item","numeric-id":3543655,"id":"Q3543655"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$233CE0E6-320E-4058-8550-6143D994E9EA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5dffe5441220fd05c9ab29a095f510d384d606b","datavalue":{"value":{"entity-type":"item","numeric-id":2945637,"id":"Q2945637"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$18870D31-9FA6-49F8-B3D0-DAE61C1BF478","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c4fd2399a3704cf83726a1162abe2d51c058ed2e","datavalue":{"value":{"entity-type":"item","numeric-id":2551314,"id":"Q2551314"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$85AD9229-7CF2-490B-853A-F2EEB4B30114","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$268CFA3C-E6F0-435D-B8DA-7E994E5C0B60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6e1f8d3bfe490f5c098b93d5a6eedb55bea55682","datavalue":{"value":{"entity-type":"item","numeric-id":5578544,"id":"Q5578544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$DAAD5AB3-2377-4596-9607-FD0AA011B688","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5f33eb85be6ac8e355bf84551001f5c2b5f1a7d0","datavalue":{"value":{"entity-type":"item","numeric-id":1887670,"id":"Q1887670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$DE33429D-121A-48D0-825A-CADC17EF4E16","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a28463bf0bf1279da28a4651925c3b9d76c0ef25","datavalue":{"value":{"entity-type":"item","numeric-id":2766536,"id":"Q2766536"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$A1491F64-E008-4CE8-A4B9-E594214A5888","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0ddd7cc078612c9199a84994e4dadb80a60e0919","datavalue":{"value":{"time":"+2018-05-22T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40354$1C93D836-34E4-4164-834F-21ECC707EAA3","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2b9da69547c51d731806cb2e50756f7d52aa7f05","datavalue":{"value":{"text":"Monadification, Memoization and Dynamic Programming","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40354$82094763-9432-4047-B561-B67293685919","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":"Q40354$BC3B39DA-7574-4159-B801-FAD208FA00E2","rank":"normal"}],"P585":[{"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":"Q40354$C65DF5B4-3EBB-4591-9C52-C9B1EE2D2DFE","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"1157f6239d5752bb0ad1cee836272bd46c6bf40f","datavalue":{"value":{"entity-type":"item","numeric-id":7360772,"id":"Q7360772"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40354$DBF94F8D-7E63-475E-900C-EC5173A4C991","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Memoization","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Memoization"}}}}}