Relations are ubiquitous in mathematics and computer science. Reflecting this, in the field of "relational and algebraic methods in computer science" relations are used in a multitude of ways, for example as models for the actions of nondeterministic programs or as models of states, such as the structured data of databases or XML documents. Sometimes it is advantageous to restrict to single-valued relations, i.e., partial functions, which can model deterministic programs or the state of allocated memory (e.g. in separation logic). Using (unrestricted) relations offers greater generality, whereas using partial functions offers greater tractability. Duality theory studies contravariant equivalences of categories and is a powerful tool used in logic. This project aims to develop duality theory for algebras of relations and algebras of partial functions. The project is organised into two main research phases, divided along relation/partial function lines: • Extending the profinite theory of monoids to profinite algebra for Kleene algebras with domain; • Developing duality for algebras of partial functions and applying it to the theory of transducers. The project has the potential to advance duality theory as applicable to verification formalisms in many directions: broadening the general theory, strengthening existing dualities, deepening our understanding of specific important dual objects, and initiating new areas of application.