Workshop on Logic, Algebra and Category Theory: LAC 2018

Modern specification languages are based on logic. For any such language there exists a specific logical system underlying the language’s features and constructions. The logic-based approach has great advantages for formal software verification, since it guarantees precision and clarity in the process of software development. On the other hand, it resulted in a proliferation of logical systems in specification theory, each tailor-made for a particular language. Essentially the same arguments and results had to be used for each of these systems, just to fit a different language. To avoid such redundancies, a unifying framework is clearly needed. One could then prove logical results in an abstract way and then apply them to concrete specification languages. Such a framework would also contribute to a deeper understanding of the causality relations between logic properties which are often hindered by the unnecessary details of concrete logics.

Category theory suggests itself as a general supporting structure, since it focuses on relations between objects rather than the precise way the objects are built. On the other hand, universal algebra plays an important role in defining the semantics of algebraic specification languages. Therefore, there exists a strong connection between logic, category theory and algebraic structures, especially in the context of formal methods, where mathematically grounded techniques are developed for modeling and verifying complex systems in various fields of computing science.