BEGIN:VCALENDAR
VERSION:2.0
X-WR-TIMEZONE:Europe/Paris
CALSCALE:GREGORIAN
PRODID:-//SPIP/Plugin Agenda//NONSGML v1.0//FR
X-WR-CALNAME;VALUE=TEXT: -- Institut de Mathématiques de Marseille\, UMR 7373
X-WR-RELCALID:http://www.i2m.univ-amu.fr/spip.php?page=article&id_article=0
BEGIN:VEVENT
SUMMARY:Valentin BLOT - Extensional and intensional semantic universes : a denotational model of dependent types
UID:20180622T115607-a123-e2401@https://www.i2m.univ-amu.fr
DTSTAMP:20180622T115607
DTSTART:20180705T110000
DTEND:20180705T123000
CREATED:20180622T115607
ATTENDEE;CN=Valentin BLOT:mailto:no-reply@math.cnrs.fr
LAST-MODIFIED:20180704T094252
LOCATION:Salle des séminaires 304-306 (3ème étage)
DESCRIPTION: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. http://valentinblot.org/pro/ Valentin BLOT [
CATEGORIES:(Séminaire Logique et Interactions|textebrut|filtrer_ical)]
URL:http://www.i2m.univ-amu.fr/Seminaire-Logique-et-Interactions?id_evenement=2401
SEQUENCE:1
STATUS:CONFIRMED
END:VEVENT