Game semantics of Martin-Löf type theory

DOI10.1017/s0960129523000154arXiv1905.00993MaRDI QIDQ6190409

Norihiro Yamada

Publication date: 5 March 2024

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

constructive mathematicsMartin-Löf type theorydependent typesgame semantics

Mathematics Subject Classification ID

Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Totality in arena games
• Lectures on the Curry-Howard isomorphism
• Domain interpretations of Martin-Löf's partial type theory
• Sequential algorithms on concrete data structures
• Constructivism in mathematics. An introduction. Volume II
• Full abstraction for idealized Algol with passive expressions
• A game semantics for generic polymorphism
• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• A game-semantic model of computation
• Locally cartesian closed categories and type theory
• Games for Dependent Types
• Abstract Böhm trees
• Games and full completeness for multiplicative linear logic
• Internal type theory
• A semantics of evidence for classical arithmetic
• Extensional and Intensional Semantic Universes
• Homotopy Type Theory: Univalent Foundations of Mathematics
• The biequivalence of locally cartesian closed categories and Martin-Löf type theories