Dependent Types for Extensive Games

DOI10.6092/ISSN.1972-5787/7517MaRDI QIDQ5195288zbMATH OpenOpenAlexFDO

Authors Pierre Lescanne

Publication date 18 September 2019

Full work available at URL https://arxiv.org/abs/1611.06101

zbMATH Keywords

coinductionCoqextensive gameinfinite gameproof assistantsequential game

Mathematics Subject Classification ID

Formalization of mathematics in connection with theorem provers (68V20) Games in extensive form (91A18)

Abstract: Extensive games are tools largely used in economics to describe decision processes ofa community of agents. In this paper we propose a formal presentation based on theproof assistant COQ which focuses mostly on infinite extensive games and theircharacteristics. COQ proposes a feature called "dependent types", which meansthat 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 agentherself. Using dependent types, we describe formally a very general class of gamesand 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 beprecisely described.

Recommendations

• Higher-order games with dependent types
• Game semantics for dependent types
• Game semantics for type soundness
• scientific article; zbMATH DE number 1808198
• Innocent game semantics via intersection type assignment systems
• Conditional cooperation: type stability across games
• Two-Level Game Semantics, Intersection Types, and Recursion Schemes
• Extended game-theoretical semantics
• A type assignment system for game semantics
• Dependent types in mathematical theory of programming

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Dependent Types for Extensive Games

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5195288)