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:7431@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20171207T110000
DTEND;TZID=Europe/Paris:20171207T123000
DTSTAMP:20241120T203951Z
URL:https://www.i2m.univ-amu.fr/evenements/a-realizability-notion-for-mso-
 over-o/
SUMMARY:Pierre Pradic (LIP\, ÉNS Lyon): A realizability notion for MSO ove
 r ω
DESCRIPTION:Pierre Pradic: Church’s synthesis problem asks whether there 
 exists a finite-state stream transducer satisfying a given input-output sp
 ecification. For specifications written in Monadic Second-Order Logic over
  infinite words\, Church’s synthesis can theoretically be solved algorit
 hmically using automata and games\, at the price of a non-elementary compl
 exity. We revisit Church’s synthesis via the Curry-Howard correspondence
  by introducing SMSO\, a non-classical subsystem of MSO\, which is shown t
 o be sound and complete w.r.t. synthesis thanks to a realizability model i
 nspired by Colin's fibration of automatas over infinite trees. Extracting 
 stream transducers from SMSO proofs is still non-elementary from an algori
 thmic point of view due to the rule of bounded comprehension.\nJoint work 
 with Colin Riba.\n\nhttp://dblp.uni-trier.de/pers/hd/p/Pradic:Pierre
CATEGORIES:Séminaire,Logique et Interactions
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:STANDARD
DTSTART:20171029T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
END:STANDARD
END:VTIMEZONE
END:VCALENDAR