  We prove a Kleene theorem for higher-dimensional automata. It states that the
languages they recognise are precisely the rational subsumption-closed sets of
finite interval pomsets. The rational operations on these languages include a
gluing composition, for which we equip pomsets with interfaces. For our proof,
we introduce higher-dimensional automata with interfaces, which are modelled as
presheaves over labelled precube categories, and develop tools and techniques
inspired by algebraic topology, such as cylinders and (co)fibrations.
Higher-dimensional automata form a general model of non-interleaving
concurrency, which subsumes many other approaches. Interval orders are used as
models for concurrent and distributed systems where events extend in time. Our
tools and techniques may therefore yield templates for Kleene theorems in
various models and applications.
