  We present abstract complexity results about Coquand and Hyland-Ong game
semantics, that will lead to new bounds on the length of first-order
cut-elimination, normalization, interaction between expansion trees and any
other dialogical process game semantics can model and apply to. In particular,
we provide a novel method to bound the length of interactions between visible
strategies and to measure precisely the tower of exponentials defining the
worst-case complexity. Our study improves the old estimates on average by
several exponentials.
