Games for dependent types

DOI10.1007/978-3-662-47666-6_3zbMATH Open1395.68177DBLPconf/icalp/AbramskyJV15OpenAlexW1863499813WikidataQ57006413 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)

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

Mathematics Subject Classification ID

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

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.

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

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 1241699 (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
• Full abstraction for PCF
• Game semantics for access control
• Games and full completeness for multiplicative linear logic
• Homotopy theoretic models of identity types
• On full abstraction for PCF: I, II and III

Cited in

(4)

• A game-semantic model of computation
• An adequacy theorem for dependent type theory
• 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)