BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//wp-events-plugin.com//7.2.3.1//EN
TZID:Europe/Paris
X-WR-TIMEZONE:Europe/Paris
BEGIN:VEVENT
UID:7265@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20180705T110000
DTEND;TZID=Europe/Paris:20180705T123000
DTSTAMP:20241120T203852Z
URL:https://www.i2m.univ-amu.fr/evenements/extensional-and-intensional-sem
 antic-universes-a-denotational-model-of-dependent-types/
SUMMARY:Valentin Blot (IRIF\, Université de Paris): Extensional and intens
 ional semantic universes: a denotational model of dependent types
DESCRIPTION:Valentin Blot: We describe a dependent type theory\, and a deno
 tational model for it\, that incorporates both intensional and extensional
  semantic universes.\nIn the former\, terms and types are interpreted as s
 trategies 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 whic
 h we may interpret an (extensional) universe type of (intensional) types. 
 A dependent game corresponds to a stable function into this domain\; we us
 e its trace to define dependent product and sum constructions as it captur
 es precisely how unfolding moves combine with the dependency to shape the 
 possible interaction in the game. Since each strategy computes a stable fu
 nction on CDS states\, we can lift typing judgements from the intensional 
 to the extensional setting\, giving an expressive type theory with recursi
 vely defined type families and type operators. We define an operational se
 mantics for intensional terms\, giving a functional programming language b
 ased on our type theory\, and prove that our semantics for it is computati
 onally adequate. By extending it with a simple non-local control operator 
 on intensional terms\, we can precisely characterize behaviour in the inte
 nsional model. We demonstrate this by proving full abstraction and full co
 mpleteness results.\n\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Valentin_Blot.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20180325T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR