Name
Abstract | ||
|---|---|---|
We present a game semantics for dependent type theory DTT with $$\\varPi $$-, $$\\varSigma $$-, intensional $$\\mathsf {Id}$$-types and finite inductive type families. The model satisfies Streicher's criteria of intensionality and refutes function extensionality. The principle of uniqueness of identity proofs is satisfied. The model is fully and faithfully complete at the type hierarchy built without $$\\mathsf {Id}$$-types. Although definability for the hierarchy with $$\\mathsf {Id}$$-types remains to be investigated, the notions of propositional equality in syntax and semantics do coincide for open terms of the $$\\mathsf {Id}$$-free type hierarchy. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-662-47666-6_3 | ICALP |
Field | DocType | Volume |
Uniqueness,Discrete mathematics,Extensionality,Inductive type,Combinatorics,Mathematical proof,Game semantics,Hierarchy,Dependent type,Type family,Mathematics | Journal | abs/1508.05023 |
ISSN | Citations | PageRank |
ICALP 2015, Part II, LNCS 9135 | 2 | 0.39 |
References | Authors | |
14 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Samson Abramsky | 1 | 3169 | 348.51 |
| Radha Jagadeesan | 2 | 2117 | 121.75 |
| Matthijs Vákár | 3 | 19 | 4.89 |