Game semantics for dependent types

DOI10.1016/J.IC.2018.02.015MaRDI QIDQ1641014zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

game semanticsdependent type theoryintensionality

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 6694181 (Why is no real title available?)
• scientific article; zbMATH DE number 1223609 (Why is no real title available?)
• scientific article; zbMATH DE number 1302058 (Why is no real title available?)
• scientific article; zbMATH DE number 1302059 (Why is no real title available?)
• scientific article; zbMATH DE number 1499102 (Why is no real title available?)
• scientific article; zbMATH DE number 860033 (Why is no real title available?)
• A categorical semantics for linear logical frameworks
• A game semantics for generic polymorphism
• Domain interpretations of Martin-Löf's partial type theory
• Extensional Constructs in Intensional Type Theory
• Faking it Simulating dependent types in Haskell
• Full abstraction for PCF
• Game semantics for access control
• Games and full completeness for multiplicative linear logic
• Games for dependent types
• Generalized algebraic theories and contextual categories
• Handbook of logic in computer science. Vol. 5: Logical and algebraic methods
• Homotopy theoretic models of identity types
• Homotopy type theory. Univalent foundations of mathematics
• Inductive families
• Internal type theory
• Least and Greatest Fixpoints in Game Semantics
• On full abstraction for PCF: I, II and III
• Probabilistic game semantics
• Typed Lambda Calculi and Applications

Cited in

(5)

• A short note on type-inhabitation: formula-trees vs. game semantics
• Dependent Types for Extensive Games
• 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
• Games for dependent types

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)