Extensional and intensional semantic universes: A denotational model of dependent types

Valentin Blot, Jim Laird

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data structures of a generalized form, and in the latter as stable functions on event domains. The concrete data structures themselves form an event domain, with which we may interpret an (extensional) universe type of (intensional) types. A dependent game corresponds to a stable function into this domain; we use its trace to define dependent product and sum constructions as it captures precisely how unfolding moves combine with the dependency to shape the possible interaction in the game. Since each strategy computes a stable function on CDS states, we can lift typing judgements from the intensional to the extensional setting, giving an expressive type theory with recursively defined type families and type operators. We define an operational semantics for intensional terms, giving a functional programming language based on our type theory, and prove that our semantics for it is computationally adequate. By extending it with a simple non-local control operator on intensional terms, we can precisely characterize behaviour in the intensional model. We demonstrate this by proving full abstraction and full completeness results.

LanguageEnglish
Title of host publicationProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
PublisherIEEE
Pages95-104
Number of pages10
VolumePart F138033
ISBN (Electronic)9781450355834
DOIs
StatusPublished - 9 Jul 2018
Event33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 - Oxford, UK United Kingdom
Duration: 9 Jul 201812 Jul 2018

Publication series

NameProceedings - Symposium on Logic in Computer Science
PublisherIEEE
ISSN (Electronic)2575-5528

Conference

Conference33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018
CountryUK United Kingdom
CityOxford
Period9/07/1812/07/18

Fingerprint

Type Theory
Forms (concrete)
Concrete Structures
Semantics
Game
Data structures
Dependent
Data Structures
Term
Concretes
Functional programming
Functional Programming
Operational Semantics
Unfolding
Operator
Computer programming languages
Programming Languages
Completeness
Trace
Model

ASJC Scopus subject areas

  • Software
  • Mathematics(all)

Cite this

Blot, V., & Laird, J. (2018). Extensional and intensional semantic universes: A denotational model of dependent types. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 (Vol. Part F138033, pp. 95-104). (Proceedings - Symposium on Logic in Computer Science). IEEE. https://doi.org/10.1145/3209108.3209206

Extensional and intensional semantic universes : A denotational model of dependent types. / Blot, Valentin; Laird, Jim.

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Vol. Part F138033 IEEE, 2018. p. 95-104 (Proceedings - Symposium on Logic in Computer Science).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Blot, V & Laird, J 2018, Extensional and intensional semantic universes: A denotational model of dependent types. in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. vol. Part F138033, Proceedings - Symposium on Logic in Computer Science, IEEE, pp. 95-104, 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK United Kingdom, 9/07/18. https://doi.org/10.1145/3209108.3209206
Blot V, Laird J. Extensional and intensional semantic universes: A denotational model of dependent types. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Vol. Part F138033. IEEE. 2018. p. 95-104. (Proceedings - Symposium on Logic in Computer Science). https://doi.org/10.1145/3209108.3209206
Blot, Valentin ; Laird, Jim. / Extensional and intensional semantic universes : A denotational model of dependent types. Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018. Vol. Part F138033 IEEE, 2018. pp. 95-104 (Proceedings - Symposium on Logic in Computer Science).
@inproceedings{efc7d116975848d2aee7d149ed5bb2f2,
title = "Extensional and intensional semantic universes: A denotational model of dependent types",
abstract = "We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data structures of a generalized form, and in the latter as stable functions on event domains. The concrete data structures themselves form an event domain, with which we may interpret an (extensional) universe type of (intensional) types. A dependent game corresponds to a stable function into this domain; we use its trace to define dependent product and sum constructions as it captures precisely how unfolding moves combine with the dependency to shape the possible interaction in the game. Since each strategy computes a stable function on CDS states, we can lift typing judgements from the intensional to the extensional setting, giving an expressive type theory with recursively defined type families and type operators. We define an operational semantics for intensional terms, giving a functional programming language based on our type theory, and prove that our semantics for it is computationally adequate. By extending it with a simple non-local control operator on intensional terms, we can precisely characterize behaviour in the intensional model. We demonstrate this by proving full abstraction and full completeness results.",
author = "Valentin Blot and Jim Laird",
year = "2018",
month = "7",
day = "9",
doi = "10.1145/3209108.3209206",
language = "English",
volume = "Part F138033",
series = "Proceedings - Symposium on Logic in Computer Science",
publisher = "IEEE",
pages = "95--104",
booktitle = "Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018",
address = "USA United States",

}

TY - GEN

T1 - Extensional and intensional semantic universes

T2 - A denotational model of dependent types

AU - Blot, Valentin

AU - Laird, Jim

PY - 2018/7/9

Y1 - 2018/7/9

N2 - We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data structures of a generalized form, and in the latter as stable functions on event domains. The concrete data structures themselves form an event domain, with which we may interpret an (extensional) universe type of (intensional) types. A dependent game corresponds to a stable function into this domain; we use its trace to define dependent product and sum constructions as it captures precisely how unfolding moves combine with the dependency to shape the possible interaction in the game. Since each strategy computes a stable function on CDS states, we can lift typing judgements from the intensional to the extensional setting, giving an expressive type theory with recursively defined type families and type operators. We define an operational semantics for intensional terms, giving a functional programming language based on our type theory, and prove that our semantics for it is computationally adequate. By extending it with a simple non-local control operator on intensional terms, we can precisely characterize behaviour in the intensional model. We demonstrate this by proving full abstraction and full completeness results.

AB - We describe a dependent type theory, and a denotational model for it, that incorporates both intensional and extensional semantic universes. In the former, terms and types are interpreted as strategies on certain graph games, which are concrete data structures of a generalized form, and in the latter as stable functions on event domains. The concrete data structures themselves form an event domain, with which we may interpret an (extensional) universe type of (intensional) types. A dependent game corresponds to a stable function into this domain; we use its trace to define dependent product and sum constructions as it captures precisely how unfolding moves combine with the dependency to shape the possible interaction in the game. Since each strategy computes a stable function on CDS states, we can lift typing judgements from the intensional to the extensional setting, giving an expressive type theory with recursively defined type families and type operators. We define an operational semantics for intensional terms, giving a functional programming language based on our type theory, and prove that our semantics for it is computationally adequate. By extending it with a simple non-local control operator on intensional terms, we can precisely characterize behaviour in the intensional model. We demonstrate this by proving full abstraction and full completeness results.

UR - http://www.scopus.com/inward/record.url?scp=85051120455&partnerID=8YFLogxK

U2 - 10.1145/3209108.3209206

DO - 10.1145/3209108.3209206

M3 - Conference contribution

VL - Part F138033

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 95

EP - 104

BT - Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018

PB - IEEE

ER -