Game semantics for dependent types

DOI10.1016/J.IC.2018.02.015zbMATH Open1395.68183OpenAlexW2553266761MaRDI QIDQ1641014FDOQ1641014

Authors: Matthijs Vákár, Radha Jagadeesan, 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

Recommendations

• Games for dependent types
• Extensional and Intensional Semantic Universes
• Kripke Semantics for Martin-Löf’s Extensional Type Theory
• Kripke Semantics for Martin-L\"of's Extensional Type Theory
• scientific article; zbMATH DE number 1956502

zbMATH Keywords

game semanticsdependent type theoryintensionality

Mathematics Subject Classification ID

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

Cites Work

• On full abstraction for PCF: I, II and III
• Full abstraction for PCF
• Handbook of logic in computer science. Vol. 5: Logical and algebraic methods
• Generalized algebraic theories and contextual categories
• Inductive families
• Homotopy theoretic models of identity types
• Title not available (Why is that?)
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Internal type theory
• Title not available (Why is that?)
• Least and Greatest Fixpoints in Game Semantics
• Title not available (Why is that?)
• Games and full completeness for multiplicative linear logic
• Typed Lambda Calculi and Applications
• Probabilistic game semantics
• Extensional Constructs in Intensional Type Theory
• Game semantics for access control
• Domain interpretations of Martin-Löf's partial type theory
• Title not available (Why is that?)
• A game semantics for generic polymorphism
• A Categorical Semantics for Linear Logical Frameworks
• Title not available (Why is that?)
• Faking it Simulating dependent types in Haskell
• Games for Dependent Types
• Title not available (Why is that?)

Cited In (4)

• A short note on type-inhabitation: formula-trees vs. game semantics
• Retracing some paths in categorical semantics: from process-propositions-as-types to categorified reals and computers
• Two-Level Game Semantics, Intersection Types, and Recursion Schemes
• Dependent Types for Extensive Games

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

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