Skip to Main content Skip to Navigation
Reports

A Foundational Framework for the Specification and Verification of Mechanism Design

Pierre Jouvelot 1, 2 Emilio Jesús Gallego Arias 3 
3 PI.R2 - Design, study and implementation of languages for proofs and programs
CNRS - Centre National de la Recherche Scientifique, Inria de Paris, UPCité - Université Paris Cité, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
Abstract : We introduce mech.v, a new framework for the specification and verification of mechanisms, implemented using the Coq interactive theorem prover and the Mathematical Components library. We provide a general definition of mechanism, a subclass capturing auctions, and a few examples of auctions including three notions of Vickrey-Clarke-Groves (VCG), proving their main incentive properties such as truthfulness with reasonable verification effort. We define and prove some more lemmas and definitions usually found in the mechanism design (MD) literature such as Pareto-optimality, rationality, dominance and Nash equilibria. We also define a mechanism refinement system, which we use to relate the implementation of an efficient version of the VCG mechanism for an online advertisement auction to the general VCG specification, allowing us to transfer the truthfulness property from the generic proof. We hope that our library can be useful as a formally verified, unambiguous reference with applications ranging from verification of deployed mechanism to education, and that this is a first step to gather interesting results and definitions from the MD literature to eventually provide a comprehensive mechanically formalized reference.
Complete list of metadata

https://hal-mines-paristech.archives-ouvertes.fr/hal-03666871
Contributor : Claire Medrala Connect in order to contact the contributor
Submitted on : Thursday, May 12, 2022 - 5:47:56 PM
Last modification on : Tuesday, September 6, 2022 - 1:27:06 PM

File

E-458.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03666871, version 1

Citation

Pierre Jouvelot, Emilio Jesús Gallego Arias. A Foundational Framework for the Specification and Verification of Mechanism Design. [Research Report] E-458.PDF, MINES ParisTech - PSL Research University. 2022. ⟨hal-03666871⟩

Share

Metrics

Record views

23

Files downloads

12