P. Aczel, Non-well-founded Sets, CSLI Lecture Notes. CSLI Publications, vol.14, 1988.

R. J. Aumann, Backward induction and common knowledge of rationality, Games and Economic Behavior, vol.8, issue.1, pp.6-19, 1995.
DOI : 10.1016/S0899-8256(05)80015-6

Y. Bertot, Filters on CoInductive Streams, an Application to Eratosthenes??? Sieve, Typed Lambda Calculus and Applications'05, pp.102-115, 2005.
DOI : 10.1007/11417170_9

URL : https://hal.archives-ouvertes.fr/inria-00070658

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

K. Binmore, Modeling Rational Players: Part I, Economics and Philosophy, vol.49, issue.02, pp.179-214, 1987.
DOI : 10.2307/1885999

K. Binmore, Modeling Rational Players: Part II, Economics and Philosophy, vol.2, issue.01, pp.9-55, 1988.
DOI : 10.1007/BF01737554

V. Capretta, Common knowledge as a coinductive modality, Reflections on Type Theory, Lambda Calculus, and the Mind, pp.51-61, 2007.

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

A. M. 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-grimal and L. Jakubiec, Certifying circuits in type theory. Formal Asp, Comput, vol.16, issue.4, pp.352-373, 2004.

G. Dowek, Les métamorphoses du calcul. Le Pommier Grand Prix of Philosophy of the French Academy, English title: The metamorphoses of computation, 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

R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi, Reasoning about Knowledge, 1995.

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

J. Y. Halpern, Substantive Rationality and Backward Induction, Games and Economic Behavior, vol.37, issue.2, pp.425-435, 2001.
DOI : 10.1006/game.2000.0838

J. Harrison, Formal proof ? theory and practice. Notices of the, pp.1395-1406, 2008.

N. Julien, Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base, Lecture Notes in Computer Science, vol.4989, pp.48-63, 2008.
DOI : 10.1007/978-3-540-78969-7_6

URL : https://hal.archives-ouvertes.fr/inria-00202744

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

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, Deconstruction of infinite extensive games using coinduction. CoRR, abs, 2009.
URL : https://hal.archives-ouvertes.fr/ensl-00376141

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

D. Martin, The determinacy of Blackwell games, The Journal of Symbolic Logic, vol.66, issue.04, pp.1565-1581, 1998.
DOI : 10.1007/BF02801569

R. Mazala, Infinite Games, Automata, Logics, and Infinite Games, pp.23-42, 2001.
DOI : 10.1007/3-540-36387-4_2

R. Milner and M. Tofte, Co-induction in relational semantics, Theoretical Computer Science, vol.87, issue.1, pp.209-220, 1991.
DOI : 10.1016/0304-3975(91)90033-X

D. Mirimanoff, Les antimonies de Russell et de Burali-Forti et leprobì eme fondamental de la théorie des ensembles, Enseignement Mathématique, vol.19, pp.37-52, 1917.

F. Nash and J. , Equilibrium points in n-person games, Proceedings of the National Academy of Sciences, pp.48-49, 1950.

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, An Introduction to Game Theory, 2004.

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

C. Pair, Concerning the syntax of ALGOL 68, Algol Bulletin, vol.31, pp.1-27, 1970.

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

D. Sangiorgi, On the origins of bisimulation and coinduction, ACM Trans. Program. Lang. Syst, vol.31, issue.4, 2009.

R. Selten, Spieltheoretische Behandlung eines Oligopolmodells mit Nachfragetrgheit . Zeitschrift für gesamte Staatswissenschaft, 1965.

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

R. C. Stalnaker, Belief revision in games: forward and backward induction, Mathematical Social Sciences, vol.36, issue.1, pp.31-56, 1998.
DOI : 10.1016/S0165-4896(98)00007-9

A. Turing, Computability and ??-definability, The Journal of Symbolic Logic, vol.42, issue.04, pp.153-163, 1937.
DOI : 10.2307/2371045

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

J. Neumann, Eine axiomatiserung der Mengenlehre Translated as An axiomatization of Set Theory in From Frege to Gödel, J. F. Math. J. van Heijenoort ed, vol.154, 1925.

J. Neumann, Zur Theorie der Gesellschaftsspiele, Mathematische Annalen, vol.100, issue.1, pp.295-300, 1928.
DOI : 10.1007/BF01448847

J. Von-neumann and O. Morgenstern, Theory of Games and Economic Behavior, 1944.

K. Weierstrass, ¨ Uber continuirliche Funktionen eines reellen Arguments, die für keinen Werth des letzteren einen bestimmten Differentialquotienten besitzen, 1872, Abhandlungen II. Gelesen in der Königl. Akademie der Wisseschaften am 18 Juli 1872, 1967.

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

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

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

S. Sgpe-coinductive, StratProf ? Prop := ? SGPE leaf : ? f :Utility fun, SGPE (?f?)

?. Sgpe, Agent )(u v : Utility) (sl sr : StratProf ), AlwLeadsToLeaf (?a,l,sl,sr?) ? SGPE sl ? SGPE sr ? s2u sl a u ? s2u sr a v ?

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