mech.v

A Coq- and Mathematical Components-based formalization project for mechanism design, mech.v, with applications to many existing mechanisms, including General VCG, VCG for Search, Combinatorial VCG, Fixed/First/Second Price, ... and their properties.

This is Work In Progress and should do not used for "final consumption".

This has been tested under Coq 8.17 and mathcomp 1.17.

Bibliography

Find below some links to bibliography and related projects:

• https://arxiv.org/abs/2104.08437 ITP 2021

• "Computer-aided verification in mechanism design" https://arxiv.org/abs/1502.04052

• "Sound Auction Specification and Implementation" https://dl.acm.org/doi/pdf/10.1145/2764468.2764511

• https://github.com/formare

• https://oaklandsok.github.io/

Documentation

• See file headers for proper description

• Contributors' Mines Paris technical report, "A Foundational Framework for the Specification and Verification of Mechanism Design" (https://www.cri.mines-paristech.fr/classement/doc/E-458.pdf)

• Poster presented at ACM 2022 Economy and Computation conference (see .pdf file)

Main contributors

• Pierre Jouvelot, Mines Paris, Université PSL
• Emilio Gallego Arias, Inria, Paris
• Lucas Massoni Sguerra, Mines Paris, Université PSL
• Zhan Jing, Jiao Tong U.