A Typed Language for Truthful One-Dimensional Mechanism Design
Date
2008-10-09
DOI
Authors
Lapets, Andrei
Levin, Alex
Parkes, David
Version
OA Version
Citation
Lapets, Andrei; Levin, Alex; Parkes, David. "A Typed Language for Truthful One-Dimensional Mechanism Design", Technical Report BUCS-TR-2008-026, Computer Science Department, Boston University, October 9, 2008. [Available from: http://hdl.handle.net/2144/3754]
Abstract
We first introduce a very simple typed language for expressing allocation algorithms that allows automatic verification that an algorithm is monotonic and therefore truthful. The analysis of truthfulness is accomplished using a syntax-directed transformation which constructs a proof of monotonicity based on an exhaustive critical-value analysis of the algorithm. We then define a more high-level, general-purpose programming language with typical constructs, such as those for defining recursive functions, along with primitives that match allocation algorithm combinators found in the work of Mu'alem and Nisan [10]. We demonstrate how this language can be used to combine both primitive and user-defined combinators, allowing it to capture a collection of basic truthful allocation algorithms. In addition to demonstrating the value of programming language design techniques in application to a specific domain, this work suggests a blueprint for interactive tools that can be used to teach the simple principles of truthful mechanism design