Games for dependent types

DOI10.1007/978-3-662-47666-6_3zbMATH Open1395.68177DBLPconf/icalp/AbramskyJV15arXiv1508.05023OpenAlexW1863499813WikidataQ57006413 ScholiaQ57006413MaRDI QIDQ3449463FDOQ3449463

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

Publication date: 4 November 2015

Published in: Automata, Languages, and Programming (Search for Journal in Brave)

Abstract: We present a model of dependent type theory (DTT) with Pi-, 1-, Sigma- and intensional Id-types, which is based on a slight variation of the category of AJM-games and history-free winning strategies. The model satisfies Streicher's criteria of intensionality and refutes function extensionality. The principle of uniqueness of identity proofs is satisfied. We show it contains a submodel as a full subcategory which gives a faithful model of DTT with Pi-, 1-, Sigma- and intensional Id-types and, additionally, finite inductive type families. This smaller model is fully (and faithfully) complete with respect to the syntax at the type hierarchy built without Id-types, as well as at the class of types where we allow for one strictly positive occurrence of an Id-type. Definability for the full type hierarchy with Id-types remains to be investigated.

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

Recommendations

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

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
• Homotopy theoretic models of identity types
• Title not available (Why is that?)
• Title not available (Why is that?)
• Games and full completeness for multiplicative linear logic
• Game semantics for access control
• Domain interpretations of Martin-Löf's partial type theory
• A game semantics for generic polymorphism
• A categorical semantics for linear logical frameworks
• Title not available (Why is that?)

Cited In (3)

• A game-semantic model of computation
• Game semantics for dependent types
• Game semantics of Martin-Löf type theory

This page was built for publication: Games for dependent types

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