Game semantics for dependent types

DOI10.1016/j.ic.2018.02.015zbMath1395.68183OpenAlexW2553266761MaRDI QIDQ1641014

Radha Jagadeesan, Matthijs Vákár, Samson Abramsky

Publication date: 14 June 2018

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://ora.ox.ac.uk/objects/uuid:7ae51c14-9cc4-41f0-8a81-291f5e5682e4

zbMATH Keywords

game semanticsintensionalitydependent type theory

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Domain interpretations of Martin-Löf's partial type theory
• Generalized algebraic theories and contextual categories
• Inductive families
• A game semantics for generic polymorphism
• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• Game Semantics for Access Control
• A Categorical Semantics for Linear Logical Frameworks
• Faking it Simulating dependent types in Haskell
• Games for Dependent Types
• Homotopy theoretic models of identity types
• Least and Greatest Fixpoints in Game Semantics
• Games and full completeness for multiplicative linear logic
• Extensional Constructs in Intensional Type Theory
• Internal type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Typed Lambda Calculi and Applications
• Probabilistic game semantics

This page was built for publication: Game semantics for dependent types