Game semantics for dependent types
We present a model of dependent type theory (DTT) with -, 1-, - and intensional Id-types, which is based on a slight variation of the (call-by-name) category of AJM-games and history-free winning well-bracketed strategies. The model satisfies Streicher’s criteria of intensionality and refutes functi...
| Main Authors: | , , |
|---|---|
| Format: | Journal article |
| Published: |
Elsevier
2018
|