Ponencia: A Category-Theoretic Framework for Algebraic Composition in Models of High-Level Computation 

Resumen de la charla:

Models of High-Level Computation (MHCs) raise the level of abstraction of classical models to describe structured interactions among a collection of abstract computing devices. In this paradigm, interactions are governed by composition mechanisms, so that compositionality emerges as a fundamental property for the inductive construction of complex computing devices from simpler ones, without the need to delve into internal structures.

In this talk, we will examine the role of algebraic composition in MHCs and introduce a category-theoretic framework that generalises the structural principles underlying control-driven composition. The framework is based on algebraic operators characterised as finite colimit constructions in a subcategory of functors with domain in a finitely generated free category. These operators enable the compositional construction of sequential, parallel, branching and iterative computing devices that are deadlock-free and exhibit a semantic separation between control flow and data flow. This separation has already been proved useful for model transformation and can also be exploited for separative formal verification. The framework further decouples composition from operational semantics, thereby enabling polymorphic behavioural interpretations. In the talk, operational semantics will be discussed through the lens of categorical Petri nets and a particular transition-system semantics. Finally, we will show how the framework gives rise to non-uniform computation capable of representing Boolean functions over inputs of arbitrary length. Holistically, the framework aims to offer a rigorous universal foundation, grounded in categorical semantics, for formally reasoning about compositional high-level computation.