Dependent Types for Extensive Games

Abstract : Extensive games are tools largely used in economics to describe decision processes of a community of agents. In this paper we propose a formal presentation based on the proof assistant COQ which focuses mostly on infinite extensive games and their characteristics. COQ proposes a feature called ``dependent types'', which means that the type of an object may depend on the type of its components. For instance, the set of choices or the set of utilities of an agent may depend on the agent herself. Using dependent types, we describe formally a very general class of games and strategy profiles, which corresponds somewhat to what game theorists are used to. We also discuss the notions of infiniteness in game theory and how this can be precisely described.
Type de document :
Pré-publication, Document de travail
2016
Liste complète des métadonnées

https://hal-ens-lyon.archives-ouvertes.fr/ensl-01391418
Contributeur : Pierre Lescanne <>
Soumis le : mardi 5 décembre 2017 - 10:11:12
Dernière modification le : mardi 16 janvier 2018 - 15:35:40

Fichiers

dependentTypesForGames.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : ensl-01391418, version 3
  • ARXIV : 1611.06101

Collections

Citation

Pierre Lescanne. Dependent Types for Extensive Games. 2016. 〈ensl-01391418v3〉

Partager

Métriques

Consultations de la notice

11

Téléchargements de fichiers

5