Uma conversa com Diana Costa (LASIGE).
In this presentation I will be making a tour through the subjects I have worked/been working on. I will start with the introduction of a four-valued Hybrid Logic and an extension to Dynamic Logic and accompanying proof-theory under the form of a Tableaux system, reminiscent of my PhD thesis. Then, a version of Concurrent Separation Logic with permission regions, where hybrid machinery (namely nominals and the satisfaction operator @) is used, as well as both strong * (no overlap) and weak * (possible overlap). Finally, a brief exposition of ongoing work: a Proof-theoretic semantics for the Logic of Bunched Implications, and in a bit more depth, a Separating Pregraph Logic, an analog to standard Separation Logic where the concept of heap is replaced with a (pre)graph, whose goal is the verification of graph algorithms.
Bio: I received my PhD in Applied Mathematics in 2019 from the University of Aveiro with a thesis on Paraconsistent Hybrid Logics. For the past three years I was a Research Fellow in the Programming Principles, Logic and Verification group at University College London, where I worked mainly with BI and Separation Logic for the verification of programs. I like many-valued approaches to deal with seemingly inconsistent/incomplete systems and working with graph structures.
