# Getting thin spans in order 

Recently, Clairambault and Forest introduced the cartesian closed
bicategory of thin spans of groupoids. It is a proof-relevant
denotational model, akin to Fiore et al's categorification of the
relational model, generalized species of structure. However, unlike
generalized species, it is concrete, in the sense that its structural
operations (composition etc) involve no quotient. It achieves this by
mimicking the bicategory of thin concurrent games, and in particular
their handling of symmetry. The interpretation of lambda-calculi in thin
spans is close to that in concurrent games, while avoiding all the
combinatorial machinery of event structures. However, thin spans only
witness *complete* states of computation, where game semantics also
record all the intermediate stages and their chronological or causal
constraints.

The proposed talk concerns a work in progress towards the construction
of a new proof-relevant denotational model, a cartesian closed
bicategory of "ordered thin spans". Ordered thin spans extend thin spans
with an additional order relation, a categorification of the inclusion
between configurations in concurrent games. The basic objects of this
bicategory are certain "ordered groupoids", groupoids with a partial
order relation *on objects* satisfying additional conditions. We will
present the construction of this new model, along with preliminary
results on its use for semantic purposes and its relationship with thin
concurrent games.