  We study first-order concatenation theory with bounded quantifiers. We give
axiomatizations with interesting properties, and we prove some normal-form
results. Finally, we prove a number of decidability and undecidability results.
