{"entities":{"Q40263":{"pageid":40319,"ns":120,"title":"Item:Q40263","lastrevid":105427775,"modified":"2026-10-09T10:08:21Z","type":"item","id":"Q40263","labels":{"en":{"language":"en","value":"Separation Logic"}},"descriptions":{"en":{"language":"en","value":"AFP entry Separation_Logic_Imperative_HOL"}},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"fc744b69c053867e7e575cee4ed6ad40702388ea","datavalue":{"value":"28549","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40263$CC8D2374-FC75-4A2D-8676-4D0FBFD9C476","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":"Q40263$FAAB4997-0F5B-48CD-B576-6D93804AF8D3","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"22af90e1cd022f13a21af7f06f3b79e38cadef48","datavalue":{"value":"https://www.isa-afp.org/entries/Separation_Logic_Imperative_HOL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40263$3A403A06-26A1-4B22-B73D-8D79A5B67E86","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40263$2E926FA8-13EF-48FE-9184-8A53A3716B12","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"95bde9084e6ca63a8492631a417b047b22c72453","datavalue":{"value":"05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40263$9BB34BE4-1C76-463D-BB51-FF6111F42CD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40263$62BC7380-3318-410A-B153-69D5C3C51A56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"541da1e359051dfcf3c498b9f1f1f8f905fbafe3","datavalue":{"value":"90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40263$B7AC0445-BD52-4E44-9423-0551205E0DEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9ccfc2ffdb7a60cd36d8dca0a4e6d9d45f5228f3","datavalue":{"value":"3","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40263$43849158-7B5B-49B1-B799-43BAD73F4577","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"24f8ba20e8ffa07910d0666302c1f09a25449c97","datavalue":{"value":"5.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40263$3251EB6E-0915-4690-B7E4-E4F70CA2426D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"09f5e0c6033338f59ef27e37d6877da0f26d9646","datavalue":{"value":"68.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40263$4F8F59ED-39DE-4D53-9DE4-1B91A40BAB64","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a8aa801742e290b2e6820d89349e86d8f23555f","datavalue":{"value":"90.0","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q40263$C8CA9737-1AFE-460B-8A33-1ABC8660E627","rank":"normal"}],"P1458":[{"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":"Q40263$48DB63A9-B83F-4003-918C-251FA3A5F6D1","rank":"normal"},{"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":"Q40263$6ED996F6-3561-4D5B-A4A8-34D4F19D7FA5","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":"Q40263$4910EEB1-7AE7-49F5-8A78-6F9B01A30DDD","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":"Q40263$1C6B4911-1A4D-4D75-AC9E-DC416CCE7FD4","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":"Q40263$A6832771-0AA5-4829-B62F-C490DDF9232C","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":"Q40263$1E4395B1-4D04-4C2E-B6DE-3CF54C1E5503","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":"Q40263$EF399BBD-41B7-474A-A145-04F4B113878C","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":"Q40263$FC630C33-4692-4033-8BDD-7570C0B3186C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7c5621c1793da546d15bfffbebaf0c15e5aa730d","datavalue":{"value":{"entity-type":"item","numeric-id":24263,"id":"Q24263"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$3E693CF0-749D-4192-A031-A511D778B4BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4ca79499c612075da87d6214d0d4c5b5998dc28e","datavalue":{"value":{"entity-type":"item","numeric-id":43957,"id":"Q43957"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$C6D04459-9335-4D13-B3A8-CA667C6E3B30","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":"Q40263$3ABE7CD1-0145-4BA9-AF1B-5F6221AAEF15","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"5a90f59e98daa7490325c2b5f9c5a5a63b8942a7","datavalue":{"value":{"entity-type":"item","numeric-id":29452,"id":"Q29452"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$5D9B9D3E-45D0-4DE4-A497-C021BA0B37F2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"73bdf83b845075653e4f87bf9bebb10f97ebc7d2","datavalue":{"value":{"entity-type":"item","numeric-id":26832,"id":"Q26832"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$E499DF54-DAA7-48FE-82C8-3D34EDB181BC","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":"Q40263$5CD294AE-266B-4EF9-A8B9-8DCA2D3F2FA9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"587eb1ff352d74d75ec39594cac10abdfc1440c2","datavalue":{"value":{"entity-type":"item","numeric-id":40265,"id":"Q40265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$C470C4AE-0665-4160-914C-5B0432F4C628","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$E67A9EF5-4F07-4199-A70D-DDB8564BB02C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"4670b60278c130cc398694b62503278740209b1d","datavalue":{"value":{"entity-type":"item","numeric-id":21794,"id":"Q21794"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$C4F9C142-C205-497D-AA37-B55210741EB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"246d8bcd4bf1600a7c6d2b07f9f11f8689d33486","datavalue":{"value":{"entity-type":"item","numeric-id":40320,"id":"Q40320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$5926FC12-9090-4BD1-A434-6678469B77AC","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":"Q40263$0529E966-F946-42C0-9B95-29BBA7712D69","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9eb6daa92cb846691116f819891169c5a3010375","datavalue":{"value":"https://isa-afp.org/entries/Separation_Logic_Imperative_HOL.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q40263$ECE56A1A-9205-452E-B02D-5CD538357FBC","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7545c5768cca6bd4b47e52bfec18c22cb81849df","datavalue":{"value":"Peter Lammich","type":"string"},"datatype":"string"},"type":"statement","id":"Q40263$6EE200B1-0DBE-4845-9923-2E2EF3B67351","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"6412c9d24b4cf7d5a3ebb0c53daae0e16020f2af","datavalue":{"value":"Rene Meis","type":"string"},"datatype":"string"},"type":"statement","id":"Q40263$716AD0AE-CE04-48B1-96EC-FDDC111259CF","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"096cbac15ddf96499a3615e7bdb622bb0b46aaf9","datavalue":{"value":"We provide a framework for separation-logic based correctness proofs of Imperative HOL programs. Our framework comes with a set of proof methods to automate canonical tasks such as verification condition generation and frame inference. Moreover, we provide a set of examples that show the applicability of our framework. The examples include algorithms on lists, hash-tables, and union-find trees. We also provide abstract interfaces for lists, maps, and sets, that allow to develop generic imperative algorithms and use data-refinement techniques. As we target Imperative HOL, our programs can be translated to efficiently executable code in various target languages, including ML, OCaml, Haskell, and Scala.","type":"string"},"datatype":"string"},"type":"statement","id":"Q40263$2DBC3BEF-D25B-4C89-B6DA-4E3879E7E4C5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d3c1819ebc3ca4c31460cf0d96175b695d4d4a32","datavalue":{"value":{"entity-type":"item","numeric-id":3087993,"id":"Q3087993"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$BB9AFBA7-41D4-4AF0-9AD6-D39234870677","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":"Q40263$3A44A140-4F79-45C8-B7F0-C701AA8BA7F3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"14d5b8e94faa47932a25c9ea28ab00e770930008","datavalue":{"value":{"entity-type":"item","numeric-id":5944309,"id":"Q5944309"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$7DAE6D66-6732-4FDF-8D35-4D9948D34DA1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6fc65e36060e1ae572d6566999dbaedabd05f274","datavalue":{"value":{"entity-type":"item","numeric-id":983522,"id":"Q983522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$017C816A-92C7-46D6-8F30-0B1AB7257266","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db7da8d17bd98f8d5a342c642c4fabe6e5f07b9b","datavalue":{"value":{"entity-type":"item","numeric-id":955386,"id":"Q955386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$AD9A9C5E-BBEB-4B29-B99E-F716C69CB4C9","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":"Q40263$C7A4FA85-4825-42BA-8E95-56CC23E54CDB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"eb5c384f83cfe304bd792549ed6786939a461655","datavalue":{"value":{"entity-type":"item","numeric-id":4783297,"id":"Q4783297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$094C1587-4ECC-4D27-998F-68E4853DA3BC","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":"Q40263$FCBAF1C3-EED3-4D4D-9313-2A43487D89D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"f0d6ccc9a00d2d1e3be7ec2239689671c14dec25","datavalue":{"value":{"entity-type":"item","numeric-id":7361918,"id":"Q7361918"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$254F8278-CF6F-4E86-852E-4788101A75FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"1518b44e9920a7e58377edf0d25bb1683f308560","datavalue":{"value":{"entity-type":"item","numeric-id":7361163,"id":"Q7361163"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$EC04448B-8035-4D0C-9CE2-E7991467E1F5","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"233b9666fd641860727eb61eeec607b4ddd3d487","datavalue":{"value":{"time":"+2012-11-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q40263$110410CA-4720-40F8-B666-4D8729248802","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"97541c0d190396924c365986dc33866fc992eb54","datavalue":{"value":{"text":"A Separation Logic Framework for Imperative HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q40263$E3C44599-EE73-4D35-8A08-1CFCA83913F0","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":"Q40263$DDAE7AE2-A5E6-4CBD-89FC-6BFECD07FCC0","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"aa8f6bd5a2b4440f838b34acf103bdf45fee4f56","datavalue":{"value":{"entity-type":"item","numeric-id":7360797,"id":"Q7360797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q40263$83AA8A2E-72BC-4CF3-AA53-913B4D4EEED4","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Separation Logic","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Separation_Logic"}}}}}