2019/04/15 by Iliano Cervesato, Sharjeel Khan, Giselle Reis +1
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.292.1
published as EPTCS 292, 2019, pp. 1-14 · In Proceedings Linearity-TLLA 2018, arXiv:1904.06159
arxiv created 2019/04/15 · arxiv updated 2019/04/16
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.