  We present a declarative and modular specification of an automated trading
system (ATS) in the concurrent linear framework CLF. We implemented it in Celf,
a CLF type checker which also supports executing CLF specifications. We outline
the verification of two representative properties of trading systems using
generative grammars, an approach to reasoning about CLF specifications.
