This directory contains four COQ scripts files:

- infinite_extensive_games.v is a development of the theory of infinite extensive games.

- escalation.v is a development of two examples: the "dollar auction" aka the "illogic game of escalation" and the "centiped" game.

- bintree.v is an example illustrating a section of [2].

- dollar_auction.v is only a development of the "dollar auction game", with two new strategy profiles (a cooperation with Matthieu Perrinel, see [2]).

The files were developed by Pierre Lescanne (with the exception of theorem SGPE_Implies_NashEq in infinite_extensive_games.v)

Those files are assocatiated with two papers.


REFERENCES

[1] Pierre Lescanne. "Deconstruction of infinite extensive games using coinduction". CoRR, http://arxiv.org/abs/0904.3528

[2] Pierre Lescanne and Matthieu Perrinel. "Escalation is rational". http://perso.ens-lyon.fr/pierre.lescanne/PUBLICATIONS/escalation_relational.pdf

Pierre Lescanne