  The goal of this paper is to propose a framework for representing and
reasoning about the rules governing a combinatorial exchange. Such a framework
is at first interest as long as we want to build up digital marketplaces based
on auction, a widely used mechanism for automated transactions. Combinatorial
exchange is the most general case of auctions, mixing the double and
combinatorial variants: agents bid to trade bundles of goods. Hence the
framework should fulfill two requirements: (i) it should enable bidders to
express their bids on combinations of goods and (ii) it should allow describing
the rules governing some market, namely the legal bids, the allocation and
payment rules. To do so, we define a logical language in the spirit of the Game
Description Language: the Combinatorial Exchange Description Language is the
first language for describing combinatorial exchange in a logical framework.
The contribution is two-fold: first, we illustrate the general dimension by
representing different kinds of protocols, and second, we show how to reason
about auction properties in this machine-processable language.
