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:8160@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20150219T110000
DTEND;TZID=Europe/Paris:20150219T120000
DTSTAMP:20241120T210049Z
URL:https://www.i2m.univ-amu.fr/evenements/a-semantic-study-of-higher-orde
 r-model-checking/
SUMMARY:Charles Grellois (LIS\, LIRICA team\, Aix-Marseille Université): A
  semantic study of higher-order model-checking
DESCRIPTION:Charles Grellois: Using higher-order recusion schemes\, one can
  model the computation flow of functional programs\, and produce trees abs
 tracting their set of executions. The higher-order model-checking problem 
 is concerned with the verification of a logical property -- typically expr
 essed in monadic second-order logic -- over this tree. A key feature of th
 is logic being that it allows to express finitary as well as infinitary pr
 operties.\nOng proved the decidability of this problem in 2006 using game 
 semantics. Since then\, other semantic approaches lead to alternate proofs
 \, each of them bringing a new semantic insight to the problem. One of the
 m\, by Kobayashi and Ong\, made use of intersection types.\nIn this talk\,
  I will explain how Paul-André Melliès and I could obtain a new proof of
  this result at the light of linear logic and of its semantics. It notably
  relies on a connection between intersection types and the exponential mod
 ality and its interpretation in models of linear logic\, but also on an ex
 tension of the latter to the infinitary framework required by this higher-
 order model-checking problem.\n\n\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Charles_Grellois.jpg
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20141026T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR