{"entities":{"Q7361005":{"pageid":31518554,"ns":120,"title":"Item:Q7361005","lastrevid":105423329,"modified":"2026-10-08T13:45:15Z","type":"item","id":"Q7361005","labels":{"en":{"language":"en","value":"Monadification, Memoization and Dynamic Programming"}},"descriptions":{"en":{"language":"en","value":"AFP entry Monad_Memo_DP"}},"aliases":{},"claims":{"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":"Q7361005$71D81348-E3FF-456C-88BB-77D846331CFA","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"8ad3851178fd4351b5225d703448b2fe1218d392","datavalue":{"value":"Simon Wimmer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361005$71075187-9E3F-49B7-9400-A2C64369C3CB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"13ea027972e16b525b8e67477a370187c840ce37","datavalue":{"value":"Shuwei Hu","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361005$C9B1884F-B66E-4D05-BF0D-8CC16CDD0A59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"78083bbf5b06a4f292e9e00ee445948e4fa51db5","datavalue":{"value":"Tobias Nipkow","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361005$9130DE4F-05AD-4975-8529-FC57676F743A","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":"Q7361005$730327DB-E326-4592-9352-21E4A3F0F5F2","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":"Q7361005$C41C93C2-FB42-4AB6-AA26-AD05E2C07D1D","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":"Q7361005$5492EA1F-8F65-4363-AE99-B942E143172E","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":"Q7361005$DA1168CC-E73D-4F28-8245-AAFE32FA04C4","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":"Q7361005$55C04189-AAC3-4372-9913-7A73A9240043","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":"Q7361005$1DC0D39B-5883-4A98-8E75-700DE0B6EBE4","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":"Q7361005$789C2441-7792-4FE5-A99E-16F44C94D67D","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":"Q7361005$20DA9C27-7DB0-4E53-85AC-41B569585BE7","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":"Q7361005$4A20DE19-487A-4438-A1CC-6E288A3D796D","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":"Q7361005$D885FF67-0B8A-49C1-9877-E0D61310B871","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":"Q7361005$8D977C2D-5D0B-44D2-B5A2-4DF52D73897C","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":"Q7361005$9AA49A6E-03F2-4654-AFC8-B52F74B42261","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":"Q7361005$F0DE8DF5-E7EB-4DE4-9024-60A6A2731671","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":"Q7361005$23A99C99-ECC3-4DEC-9594-A3DA65699897","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":"Q7361005$841EB464-38D9-4E5B-8FA1-B61E063EBAD6","rank":"normal"}],"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"609a860daa4811f3d51045a7585b1a0d1fe29af8","datavalue":{"value":"28640","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361005$01F0B473-08D8-41B3-A03B-B918B54D1B3A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361005$CD2CEC67-9142-406E-8B78-9FCBDC21EEC5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a8aa801742e290b2e6820d89349e86d8f23555f","datavalue":{"value":"90.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q7361005$120F37DA-4EFE-4CBE-B5AD-8E988B5C1F8E","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":"Q7361005$C78CE839-E575-4592-B7D7-2DC12CDF9C3D","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":"Q7361005$4BE5926B-9D3D-424C-A189-FA1EB6FA03B4","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":"Q7361005$4D95F6E7-7034-48A1-A30A-245ECC18D53D","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":"Q7361005$F668C36A-99B2-436A-A4C8-42534813EBDA","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":"Q7361005$497A6BEE-76BE-41B3-9619-65EE4496F625","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":"Q7361005$38725871-A50F-4C7B-8F2C-07063B1F5E94","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":"Q7361005$216E1428-E7A1-4407-9732-0528F2A6A93E","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":"Q7361005$836B17D3-FD36-40DE-8FAC-46CF7885D2D3","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":"Q7361005$F48F8BD1-47F0-4B85-92E1-D778441D8666","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Monadification, Memoization and Dynamic Programming","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Monadification,_Memoization_and_Dynamic_Programming"}}}}}