Here we include the supplementary materials accompanying the paper 'The Design and Regulation of Exchanges: A Formal Approach'.

The file 'additional.pdf' consists of the main definitions, lemmas, theorems, and the algorithm of the paper along with the corresponding Coq statements that are used in the formalization.

The 'formalization' folder consists of the Coq formalization of our results. Read the 'README.txt' in that folder to know more about compiling and running the code.

The 'application' folder consists of the OCaml program 'Checker.ml' which can be used to detect errors in an algorithm implementing continuous double auctions. We include example data on which this program can be run on. Read the 'README.txt' file in the folder to see how to compile the program and run the demonstration.