{"entities":{"Q7361144":{"pageid":31518971,"ns":120,"title":"Item:Q7361144","lastrevid":105363239,"modified":"2026-10-07T13:34:47Z","type":"item","id":"Q7361144","labels":{"en":{"language":"en","value":"Refinement for Monadic Programs"}},"descriptions":{"en":{"language":"en","value":"AFP entry Refine_Monadic"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"bfdb13edc4bd81a76ab0c8ccc36f0f2736a36ee1","datavalue":{"value":"https://isa-afp.org/entries/Refine_Monadic.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361144$96B2A589-EC08-4B43-B09B-C7A9818400AA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ba2e2ba7c86631c6257f9147613e92ee6710f171","datavalue":{"value":{"time":"+2012-01-30T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361144$441A5624-90E0-4FCC-A717-4F74CE189F97","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7545c5768cca6bd4b47e52bfec18c22cb81849df","datavalue":{"value":"Peter Lammich","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361144$8C081EB1-E9F2-4F4B-9A8F-BC9530F83DD4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"d9121cdaa427d4817a016ad8c7f86d1791c246ad","datavalue":{"value":{"text":"Refinement for Monadic Programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361144$FE6B9121-FB78-465B-A7D4-5AD63D4B850D","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"20ba7ef800d9efb4c9c57997a9adb21274cd6b50","datavalue":{"value":"We provide a framework for program and data refinement in Isabelle/HOL. The framework is based on a nondeterminism-monad with assertions, i.e., the monad carries a set of results or an assertion failure. Recursion is expressed by fixed points. For convenience, we also provide while and foreach combinators. The framework provides tools to automatize canonical tasks, such as verification condition generation, finding appropriate data refinement relations, and refine an executable program to a form that is accepted by the Isabelle/HOL code generator. This submission comes with a collection of examples and a user-guide, illustrating the usage of the framework.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361144$E020E8BD-6127-46C9-ABA7-B107D056D420","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"5d1176d6dc531102187fc93e4f8db95105eea855","datavalue":{"value":{"entity-type":"item","numeric-id":5944217,"id":"Q5944217"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$9206310C-D57A-4DE0-9822-838C0B4C1525","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c3877a1f64445e2be38ffa92491ece3830dcf80","datavalue":{"value":{"entity-type":"item","numeric-id":916409,"id":"Q916409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$64549C4B-2495-4491-B1AF-2A48180F2756","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"79e807f14dcd5f9ad4f6bbeb1f8ea3c4bbb7d6d4","datavalue":{"value":{"entity-type":"item","numeric-id":4396958,"id":"Q4396958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$E54279AF-9A94-4D7B-9ED6-61776EB0FBB5","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":"Q7361144$1E59814E-98A1-4F80-9B12-01D389612B91","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a386259d7b6de278f96d59178a0ebe00c941a927","datavalue":{"value":{"entity-type":"item","numeric-id":3543657,"id":"Q3543657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$32504E07-5A92-4026-B9A7-4E27FB6569FD","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":"Q7361144$AF585C18-A606-4721-885E-20523F1FA5F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db463348657cf41d5ff4d422c54e0c686e6e5dfc","datavalue":{"value":{"entity-type":"item","numeric-id":2554952,"id":"Q2554952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$141DA074-EC61-46CC-83AF-1544A37F4EC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22a5a326924c9f9f3cf0f5061fb0ff950ccfad0d","datavalue":{"value":{"entity-type":"item","numeric-id":5747660,"id":"Q5747660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$ADC9C578-FDE5-4350-8DB4-A26BFD596BEF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4b2c4f754b554fd3722211419d83d8e37139cfb4","datavalue":{"value":{"entity-type":"item","numeric-id":3024879,"id":"Q3024879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$ADEB104B-D862-4F98-B0A0-0D328C0BEF85","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"25282e1f0c1e0eccc5ae4ce78bc688548d8c67f5","datavalue":{"value":{"entity-type":"item","numeric-id":396975,"id":"Q396975"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$9C91363B-A600-4C60-930D-E1590903F008","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"cbc05b7ff29191db20dc48a43ae02a396f221bf9","datavalue":{"value":{"entity-type":"item","numeric-id":3758891,"id":"Q3758891"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$CEB99485-856B-4595-8A8C-515B82377D3E","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":"Q7361144$79B08C91-2BCD-46EE-97DC-D4E875328505","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ff736e839f0888701774c765c625cde94f58c926","datavalue":{"value":{"entity-type":"item","numeric-id":3221388,"id":"Q3221388"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$C0015C65-4446-44F1-8EB2-E1E5E817F665","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a24bd10a27e1b8e759cf20e25bbc96fc409e8f8","datavalue":{"value":{"entity-type":"item","numeric-id":4127356,"id":"Q4127356"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$F28D401F-C861-4614-9DCF-C542B9463A8C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"19f6c194330051269cbb2031658aa6b4220e257c","datavalue":{"value":{"entity-type":"item","numeric-id":4702189,"id":"Q4702189"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$C2B71FF6-19D3-440B-8DB6-1D2FEF30311F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1a2d092d6968083a4fed19c68d859d36b85e3127","datavalue":{"value":{"entity-type":"item","numeric-id":4250671,"id":"Q4250671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$4F9044B1-9D42-4431-9596-0D2C638D20BD","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":"Q7361144$94446329-6D3D-45EC-83DF-30EAC5D19332","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":"Q7361144$248EA78D-1867-46D3-8EBF-9FD6F6F64F78","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"65dbfb47d0b5da65bd2cdfbc8cab28721a9f7690","datavalue":{"value":{"entity-type":"item","numeric-id":7360803,"id":"Q7360803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361144$B72789C8-978A-4C94-82C5-917EE678A0BF","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":"Q7361144$E3DEE028-BEFE-4C84-9815-EC877CCB9017","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Refinement for Monadic Programs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Refinement_for_Monadic_Programs"}}}}}