Higher-order games with dependent types

DOI10.1016/j.tcs.2023.114111arXiv2212.07735MaRDI QIDQ6049932

Martín Hötzel Escardó, Paulo Oliva

Publication date: 18 September 2023

Published in: Theoretical Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

optimal strategiessubgame perfect equilibriumAgdacomputational game theorydependent type theoryselection function

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cites Work

• Unnamed Item
• Unnamed Item
• The equivalence of bar recursion and open recursion
• Sequential games and optimal strategies
• Exhaustible sets in higher-type computation
• Selection functions, bar recursion and backward induction
• Computational Interpretations of Analysis via Products of Selection Functions
• The Peirce Translation and the Double Negation Shift
• THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT
• Compositional Game Theory
• Dependent Types at Work
• Parametrized bar recursion: a unifying framework for realizability interpretations of classical dependent choice
• BAR RECURSION AND PRODUCTS OF SELECTION FUNCTIONS
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Smart Choices and the Selection Monad

This page was built for publication: Higher-order games with dependent types