Formalization of Automated Trading Systems in a Concurrent Linear Framework

Iliano Cervesato
(Carnegie Mellon University)
Sharjeel Khan
(Carnegie Mellon University)
Giselle Reis
(Carnegie Mellon University)
Dragiša Žunić
(Carnegie Mellon University)

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.

In Thomas Ehrhard, Maribel Fernández, Valeria de Paiva and Lorenzo Tortora de Falco: Proceedings Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA 2018), Oxford, UK, 7-8 July 2018, Electronic Proceedings in Theoretical Computer Science 292, pp. 1–14.
Published: 15th April 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: