Title: A Typed Language for Truthful One-Dimensional Mechanism Design

Authors: Andrei Lapets (Boston University), Alex Levin (MIT), David C. Parkes (Harvard University)

Date: October 9, 2008

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. 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.