S. Abramsky and R. Jagadeesan, Abstract, The Journal of Symbolic Logic, vol.417, issue.02, pp.543-574, 1994.
DOI : 10.1007/BF01622878

R. Affeldt, M. Tanaka, and N. Marti, Formal Proof of Provable Security by Game-Playing in a Proof Assistant, ProvSec, pp.151-168, 2007.
DOI : 10.1007/978-3-540-75670-5_10

Y. Bertot, Affine functions and series with co-inductive real numbers, Mathematical Structures in Computer Science, vol.17, issue.01, pp.37-63, 2007.
DOI : 10.1017/S0960129506005809
URL : https://hal.archives-ouvertes.fr/inria-00001171

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development Coq'Art: The Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

A. M. Colman, Rational Models of Cognition, chapter Rationality assumptions of game theory and the backward induction paradox, pp.353-371, 1998.

M. Andrew and . Colman, Game theory and its applications in the social and biological sciences, 1999.

T. Coquand, Infinite objects in type theory, Lecture Notes in Computer Science, vol.806, pp.62-78, 1993.
DOI : 10.1007/3-540-58085-9_72

S. Coupet, An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions, Journal of Logic and Computation, vol.13, issue.6, pp.801-813, 2003.
DOI : 10.1093/logcom/13.6.801

S. Coupet-grimal and L. Jakubiec, Certifying circuits in Type Theory, Formal Aspects of Computing, vol.16, issue.4, pp.352-373, 2004.
DOI : 10.1007/s00165-004-0048-3

C. Daskalakis, P. W. Golberg, and C. H. Papadimitriou, The complexity of computing a Nash equilibrium, Communications of the ACM, vol.52, issue.2, pp.89-97, 2009.
DOI : 10.1145/1461928.1461951

G. Dowek, Les métamorphoses du calcul. Le Pommier, 2007.

H. D. Ebbinghaus and J. Flum, Finite Model Theory, 1995.

R. Fagin, Finite-model theory - a personal perspective, Theoretical Computer Science, vol.116, issue.1, pp.3-31, 1993.
DOI : 10.1016/0304-3975(93)90218-I
URL : http://doi.org/10.1016/0304-3975(93)90218-i

G. Frege, From Frege to Gdel, chapter Concept Script, 1967.

H. Gintis, Game Theory Evolving: A Problem-Centered Introduction to Modeling Strategic Interaction, 2000.

J. Girard, Locus solum: From the rules of logic to the logic of rules, Mathematical. Structures in Comp. Sci, vol.11, issue.3, pp.301-506, 2001.

W. Harold and . Kuhn, Extensive games and the problem of information. Contributions to the Theory of Games II, 1953.

W. Harold and . Kuhn, Classics in Game Theory, 1997.

W. Leininger, Escalation and Cooperation in Conflict Situations: The Dollar Auction Revisited, Journal of Conflict Resolution, vol.33, issue.2, pp.231-254, 1989.
DOI : 10.1177/0022002789033002003

P. Lescanne, Mechanizing common knowledge logic using COQ, Annals of Mathematics and Artificial Intelligence, vol.13, issue.2, pp.15-43, 2007.
DOI : 10.1007/s10472-006-9042-1
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.96.8833

K. Lorenz and P. Lorenzen, Dialogische Logik, 1978.

S. Merz, Weak Alternating Automata in Isabelle/HOL, Lecture Notes in Computer Science, vol.1869, pp.424-441, 2000.
DOI : 10.1007/3-540-44659-1_26

R. Milner, Communication and concurrency. Prentice-Hall International Series in Computer Science, 1989.

. Molì-ere, The middle-class gentleman ? wikisource, the free library [Online; accessed 19, 2008.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.

N. Nisan, T. Roughgarden, E. Tardos, and V. V. Vazirani, Algorithmic Game Theory, 2007.
DOI : 10.1017/CBO9780511800481

B. O. Neill, International Escalation and the Dollar Auction, Journal of Conflict Resolution, vol.30, issue.1, pp.33-50, 1986.
DOI : 10.1177/0022002786030001003

M. J. Osborne and A. Rubinstein, A Course in Game Theory, 1994.

M. J. Osborne, An Introduction to Game Theory, 2004.

S. Owre, J. M. Rushby, and N. Shankar, PVS: A prototype verification system, 11th International Conference on Automated Deduction (CADE), pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217

D. Park, Concurrency and automata on infinite sequences, Theoretical Computer Science, pp.167-183, 1981.
DOI : 10.1007/BFb0017309

R. W. Rosenthal, Games of perfect information, predatory pricing and the chain-store paradox, Journal of Economic Theory, vol.25, issue.1, pp.92-100, 1981.
DOI : 10.1016/0022-0531(81)90018-1

R. Stéphane-le, Abstraction and Formalization in Game Theory, Ecole normale supérieure de Lyon (France), 2008.

M. Shubik, The Dollar Auction game: a paradox in noncooperative behavior and escalation, Journal of Conflict Resolution, vol.15, issue.1, pp.109-111, 1971.
DOI : 10.1177/002200277101500111

L. Shustek, InterviewDonald Knuth: A life's work interrupted, Communications of the ACM, vol.51, issue.8, pp.31-37, 2008.
DOI : 10.1145/1378704.1378715

J. Van-benthem, Logic in Games, 2006.

R. Vestergaard, A constructive approach to sequential Nash equilibria, Information Processing Letters, vol.97, issue.2, pp.46-51, 2006.
DOI : 10.1016/j.ipl.2005.09.010

R. Vestergaard, P. Lescanne, and H. Ono, Pierre lescanne and hiroakira ono, Japan InsT. of Science and Technology, 2006.

?. Ltlleft, ? (a:Agent )(sl : Strategy) (sr :Strategy), LeadsToLeaf sl ? LeadsToLeaf (? a,l,sl,sr?)

?. Ltlright, ? (a:Agent )(sl : Strategy) (sr :Strategy), LeadsToLeaf sr ? LeadsToLeaf (? a,r,sl,sr?)

. @bullet-?a-s, LeadsT oLeaf s ? ?u : U tility, s2u s a u. ? ?a u v s, LeadsT oLeaf s ? s2u s a u ?

C. Alwleadstoleaf, AlwLeadsToLeaf (?f?) ? ALtL : ? (a:Agent )(c:Choice)(sl sr :Strategy), LeadsToLeaf (?a,c,sl,sr?) ? AlwLeadsToLeaf sl ?AlwLeadsToLeaf sr ? AlwLeadsToLeaf (?a,c,sl,sr?)

S. Coinductive, ?. Strategy, and . Prop, = ? SGPE leaf : ? f :Utility fun, SGPE (?f?) ? SGPE left : ? (a:Agent )(u v : Utility) (sl sr : Strategy), AlwLeadsToLeaf (?a,l,sl,sr?) ? SGPE sl ? SGPE sr ?

?. Sgpe, ? (a:Agent ) (u v :Utility) (sl sr : Strategy), AlwLeadsToLeaf (?a,r,sl,sr?) ? SGPE sl ? SGPE sr ?