Extraction of structured programs from specification proofs

We present a method using an extended logical system for obtaining programs from specifications written in a sublanguage of CASL. These programs are “correct” in the sense that they satisfy their specifications. The technique we use is to extract programs from proofs in formal logic by techniques due to Curry and Howard. The logical calculus, however, is novel because it adds structural rules corresponding to the standard ways of modifying specifications: translating (renaming), taking unions, and hiding signatures. Although programs extracted by the Curry-Howard process can be very cumbersome, we use a number of simplifications that ensure that the programs extracted are in a language close to a standard high-level programming language. We use this to produce an executable refinement of a given specification and we then provide a method for producing a program module that maximally respects the original structure of the specification. Throughout the paper we demonstrate the technique with a simple example.

Full surplus extraction with dominant strategies

In this note I consider the fuI! surplus extraction in an auction with private but possibly correlated values. I show that fuI! extraction in the continuum of types case is not possible in general. Neither is approximate fuI! surplus extraction if the sel!er is budget constrained.

Social norms and money

In an economy where there is no double coincidence of wants and without recordkeeping of past transactions, money is usually seen as the only mechanism that can support exchange. In this paper, we show that, as long as the population is finite and agents are sufficiently patient, a social norm establishing gift-exchange can substitute for money. Notwithstanding, for a given discount factor, the growth of the population size eventually leads to the breakdown of the social norm, while money still works. 1 Introduction