Print Email Facebook Twitter Proving functional correctness of monadic programs using separation logic Title Proving functional correctness of monadic programs using separation logic Author Clark, Liam (TU Delft Electrical Engineering, Mathematics and Computer Science) Contributor Krebbers, Robbert (mentor) Degree granting institution Delft University of Technology Programme Computer Science Date 2022-12-02 Abstract Interaction trees are an active development in representing effectful and impure pro- grams in the Coq proof assistant. Examples of programs they can represent are programs that use: mutable state, concurrency and general recursion. Besides representing these programs we also want to reason about and verify these programs using separation logic. That is the purpose of this thesis. More technically speaking interaction trees are new way to do shallow embeddings in the Coq proof assistant. They are a coinductive variant of the free monad and come with the usual constructions of events and event handlers. The aim of interaction trees is to represent impure programs and potentially non-terminating programs in their environment. Interaction trees are, in contrast to relational operational semantics, executable by interpretation or program extraction. Interaction trees come with a framework for reasoning about their behavior based on equivalency up to weak bisimulation. An open problem is to reason about interaction trees utilizing a separation logic rather than weak bisimulation. We developed Pothos as a solution to this problem. Pothos has an Iris based concurrent separation logic for interaction trees. We address the problem in a non-extensible setting, with mutable state, non-termination and concur- rency as our chosen effects. Pothos inherits all the executable properties from interaction trees and includes a novel relation of Iris’s step-index with coinductive types. We have proven our logic to be sound and include a case study of a spin lock library. The case study shows that our logic is both non-trivial and can utilize the standard Iris patterns for concurrency. Subject Separation Logicfunctional correctnessIrisInteraction treesCoq To reference this document use: http://resolver.tudelft.nl/uuid:e1a0ae3a-df80-413c-b3b7-54efa6dfac17 Part of collection Student theses Document type master thesis Rights © 2022 Liam Clark Files PDF thesis.pdf 564.59 KB Close viewer /islandora/object/uuid:e1a0ae3a-df80-413c-b3b7-54efa6dfac17/datastream/OBJ/view