Projects per year
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 nonlocal 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.
Original language  English 

Title of host publication  Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 
Publisher  IEEE 
Pages  95104 
Number of pages  10 
Volume  Part F138033 
ISBN (Electronic)  9781450355834 
DOIs  
Publication status  Published  31 Jul 2018 
Event  33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018  Oxford, UK United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018 
Publication series
Name  Proceedings  Symposium on Logic in Computer Science 

Publisher  IEEE 
ISSN (Electronic)  25755528 
Conference
Conference  33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018 

Country/Territory  UK United Kingdom 
City  Oxford 
Period  9/07/18 → 12/07/18 
ASJC Scopus subject areas
 Software
 General Mathematics
Fingerprint
Dive into the research topics of 'Extensional and intensional semantic universes: A denotational model of dependent types'. Together they form a unique fingerprint.Projects
 2 Finished

Semantic Types for Verified Program Behaviour
Engineering and Physical Sciences Research Council
28/02/14 → 31/07/17
Project: Research council

Semantic Structures for HigherOrder Information Flow
Engineering and Physical Sciences Research Council
20/06/10 → 19/06/12
Project: Research council
Profiles

James Laird
Person: Research & Teaching