{"entities":{"Q40265":{"pageid":40321,"ns":120,"title":"Item:Q40265","lastrevid":105429227,"modified":"2026-10-09T10:11:33Z","type":"item","id":"Q40265","labels":{"en":{"language":"en","value":"Refinement Monadic"}},"descriptions":{"en":{"language":"en","value":"AFP entry Refine_Monadic"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"54d5dfd1e33206e98b9770bf6efcbcef2008bc6c","datavalue":{"value":"28551","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$909F0F0A-23E0-4754-9156-ACC7D8044DD1","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":"Q40265$838C2198-482F-41BB-B1C4-6FBE1F7AB3CD","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"e224d8597f515ec39fd7b6bc149e11f219025b2c","datavalue":{"value":"https://www.isa-afp.org/entries/Refine_Monadic.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40265$96D9E2BF-DB05-4234-8B9E-C531DD1894FA","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"95bde9084e6ca63a8492631a417b047b22c72453","datavalue":{"value":"05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$9C82F4A0-81EE-4036-BC88-379F20A91C57","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3caa64e9b44e0e6a95be04e9d18f7428dc349506","datavalue":{"value":"34","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$FAEB00B4-3C56-4615-ACDD-07CA133BAEF7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a104733b1e30d91f56342777dc887a3edbb9e05f","datavalue":{"value":"65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$78CF0D11-DC52-4952-9B97-F0681FF3FD3A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$C610378D-663A-4DC9-AB7B-76915A271531","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"541da1e359051dfcf3c498b9f1f1f8f905fbafe3","datavalue":{"value":"90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$BB603075-F4C3-4955-B123-AB447950E9E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"01c8c566de1600f59b5f8122a428964fb913122a","datavalue":{"value":"37","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$B20AF491-E3F5-4A1A-A0F5-98F802056C68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d524cbea14b3375266fe3893cb26a33f13ae791e","datavalue":{"value":"5","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$CBE18D70-621D-4ABF-BC75-489C5A82497D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"237fdb40fba6ca47071c72c98b6815ef548d522f","datavalue":{"value":"34.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$F3CA7E6E-F4CE-457E-9B4C-887CD18DE826","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"467910eb92f3fefb5ab991704afbc9c141aad063","datavalue":{"value":"65.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$6050D4A3-B82C-489E-951B-F14AE922B049","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$581CED2A-ADE2-4364-AE6C-1E3DE68DE2AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a8aa801742e290b2e6820d89349e86d8f23555f","datavalue":{"value":"90.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$68D4120D-9D95-4DA4-845A-F66D297D4671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"87a555a1b2e01f4326be258f32691549082cf63e","datavalue":{"value":"37.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40265$EA03E8E0-01AF-41B3-A9A3-C82168E6773A","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$24578913-78AA-4376-A8D9-AEB65449BA1B","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":"Q40265$C922A8A9-CC59-4A82-8FA9-CA6F92074E8B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ac6e4b2309e3317f96b1f72a4f626411283f5bc5","datavalue":{"value":{"entity-type":"item","numeric-id":40629,"id":"Q40629"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$C49D9B95-5C3D-4FBD-BF70-B1C1C9510FF1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$183744F5-C1CE-47C8-B210-CE000A53D8C4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"a5226fd137c2167e439294ca4cdc09da6fe13411","datavalue":{"value":{"entity-type":"item","numeric-id":40324,"id":"Q40324"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$3673A565-370C-446D-946B-05528B3D14DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"07eb0f28b45c8f9b5cf112bbf02e95717fb938ca","datavalue":{"value":{"entity-type":"item","numeric-id":25202,"id":"Q25202"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$A90B1AD9-472C-4B38-951D-EF3C830D4AB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$F0BC1AB2-4A5A-4477-BE30-BBB76B55B6DD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"27b35591f9a1d87570b3e9ffb19e51ff7cd09a28","datavalue":{"value":{"entity-type":"item","numeric-id":40544,"id":"Q40544"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$6613DE23-683C-40AB-A57B-27C8A4A686A8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$7C8A1795-1E02-4619-98FD-1141B324BCFB","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":"Q40265$A3520A5B-25B8-44CC-AF5B-28C34F611C49","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4eea1e5549472c93f3282a38917960fdec6b61a1","datavalue":{"value":{"entity-type":"item","numeric-id":24733,"id":"Q24733"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$758D5AD3-1BF8-413D-887C-85246BD328AA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"845fea984bd3d6706acc856d0595755051e72c0c","datavalue":{"value":{"entity-type":"item","numeric-id":40263,"id":"Q40263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$4D68B9A7-0227-4B38-A6F1-E11043F0B555","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ccca80b6de24b80a4ce2a4ab4e48d31e9686f36a","datavalue":{"value":{"entity-type":"item","numeric-id":40262,"id":"Q40262"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$402269C6-7782-4469-B206-038433D5753C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"e600fcf4c16bf9bbec6afc7a64801eb6824b335c","datavalue":{"value":{"entity-type":"item","numeric-id":40264,"id":"Q40264"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$06EC796B-5F3E-4C95-BC88-246B19478554","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"aedeaf0144ca38f7cb9a3b8f0e43e0ed5b0f0353","datavalue":{"value":{"entity-type":"item","numeric-id":40283,"id":"Q40283"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$2F9349A6-A43A-4C4E-96FA-112D4A2C692A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"fb0918295880c75ce7e6107c7f8260e1eb005ccf","datavalue":{"value":{"entity-type":"item","numeric-id":40284,"id":"Q40284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$629D6D37-4168-4D81-937A-C2F5C2B3BFB8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"5e206e7a803121c179c257c0b4386d68cd679bdc","datavalue":{"value":{"entity-type":"item","numeric-id":40949,"id":"Q40949"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$061CA2A4-3D9B-417D-B072-24540A97DBAF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ce995af0d54f8ab3594278c155d6ae4d6e3a6165","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$B9322764-D049-49BF-9803-DFB2C8589F54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"f70e8f897325b539c702d8d7cb97dfafe554224c","datavalue":{"value":{"entity-type":"item","numeric-id":32823,"id":"Q32823"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$A1066FAD-01DD-44C3-94D5-76D9E6247AE3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"9ad8338290e864661fc95f2a66261cf7e07a407c","datavalue":{"value":{"entity-type":"item","numeric-id":32822,"id":"Q32822"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40265$18C8A7AC-F0DD-448C-9AD9-3FE144831E9A","rank":"normal"}],"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":"Q40265$CC34FF29-F89F-4520-BDED-68101F071029","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7545c5768cca6bd4b47e52bfec18c22cb81849df","datavalue":{"value":"Peter Lammich","type":"string"},"datatype":"string"},"type":"statement","id":"Q40265$DAD6456F-0ABD-478B-A724-EF979D4C0873","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":"Q40265$E93CB81D-B136-4642-B4D0-CEF97ACBF48C","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":"Q40265$0B622D46-375C-46E9-BBB2-F2ED07730072","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":"Q40265$A96FA845-223C-46A1-85E9-E5F2361E1DAE","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":"Q40265$59017167-D77D-45BF-BBF7-1C5EFEA07EEC","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":"Q40265$9F00CAE5-0BFC-4200-8FCC-B3227AA4F882","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":"Q40265$CF0925FD-DE3C-496C-9096-65AB4C4D30AE","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":"Q40265$FBD0F512-0C51-4B3A-B8AA-7DA0D2F06C11","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":"Q40265$91235F48-2027-400C-AD97-BF1728FAA1F2","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":"Q40265$178E8EC1-B55A-4383-BCB1-4A0C8273342E","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":"Q40265$906118F5-93F7-451D-A5B6-F2D7E9B663F2","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":"Q40265$BBC87B6C-6F58-4EEE-A763-44080637A934","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":"Q40265$E9C2B2D4-FAED-4B08-8CA2-AED7FAD94509","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":"Q40265$B0C11C6C-D432-431E-8257-0F05E82C8B81","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":"Q40265$218F14E0-B45D-4165-B06C-3C8443560DA9","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":"Q40265$0C091ED1-E925-4185-8447-94B8BFD4FC83","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":"Q40265$46A6FACB-36E9-4034-A649-6A02C18C6301","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":"Q40265$8BBFD1C2-A45C-44EE-8A37-217F28066D07","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":"Q40265$B2E46085-AEA1-4D51-8E91-3906E2AE5C7A","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":"Q40265$FA2DC394-5799-42BB-B189-7C84C6B98B78","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":"Q40265$62E11FCD-3D86-4984-8788-125DD538767F","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":"Q40265$898915E4-E38B-4F38-858F-C6C493B914C8","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":"Q40265$6BA856BF-3227-4B0D-96D6-BE48847105CD","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Refinement Monadic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Refinement_Monadic"}}}}}