UTP and Institutions: A Unified Semantic Foundation

Dec 17 14:00 ₂₀₂₅

Abstract: Modern software and cyber-physical systems are intrinsically heterogeneous, combining discrete, continuous, probabilistic and human-in-the-loop components. Unifying Theories of Programming (UTP) provides rich, relational models of programs, supported by a refinement calculus and healthiness conditions. In contrast, Institution theory offers a logic-independent, categorical framework for heterogeneous specification and satisfaction. Yet these two influential foundations developed mainly in isolation. This talk proposes a semantic bridge between them by treating UTP theories as Institutions and wiring them together via institution (co)morphisms induced by UTP Galois connections. Signatures become UTP alphabets, sentences are healthy predicates or designs, models are programs, and satisfaction is refinement. We explore two proposals: first, replacing UTP's relational base by institutional semantics, analysing the impact on refinement, theory composition and mechanisation. Second, a hybrid framework in which UTP retains its concrete relational semantics but is organised institutionally as a "logic of logics". The outlook is a semantic "UTP supermarket" structured by institutional (co)morphisms, supporting modular, heterogeneous verification across paradigms such as reactive, probabilistic and hybrid systems and enabling tighter integration of tools like Isabelle/UTP with multi-logic environments.