On March 21, 2024 at 14:00 EET, Natalia Ozunu (University of Bucharest) will give a talk in the Logic Seminar.
Title: Modal logic for program specification
Abstract:
We developed a many-sorted hybrid polyadic modal logic, which allows us to define both the syntax of a programming language and its evaluation context. Consequently, in the syntactic layer of our system, we represent a programming language and its operational semantics such that a program execution is represented as a deductive sequence of formulas having appropriate sorts. Our goals were to define an expressive and flexible system based on a classically developed many-sorted modal logic, such that one can perform both program execution and verification. We started with a generalization of the already existing approaches on many-sorted modal logic, and we continued with various forms of hybridization. At each stage we proved completeness theorems, we analyzed the theoretical properties of our logics, and we provided relevant examples.
The talk will take place physically at FMI (Academiei 14), Hall 214 “Google”.