BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//labri.fr//NONSGML kigkonsult.se iCalcreator 2.41.92//
CALSCALE:GREGORIAN
METHOD:PUBLISH
UID:469155d8-88f8-49b2-80ed-16cafdeb73ba
X-WR-CALNAME:[MTV] Charles Grellois (LIS) - Verification of (probabilistic)
  functional programs
X-WR-TIMEZONE:Europe/Paris
BEGIN:VTIMEZONE
TZID:Europe/Paris
TZUNTIL:20231029T010000Z
BEGIN:STANDARD
TZNAME:CET
DTSTART:20211031T030000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RDATE:20221030T030000
END:STANDARD
BEGIN:DAYLIGHT
TZNAME:CEST
DTSTART:20210328T020000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RDATE:20220327T020000
RDATE:20230326T020000
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
UID:469155d8-88f8-49b2-80ed-16cafdeb73ba
DTSTAMP:20260426T065348Z
CLASS:PUBLIC
DESCRIPTION:In a functional program\, a function may take an argument that 
 is itself... a function. When it comes to model-checking\, that implies th
 at the tree of (potential) execution traces of a program is not regular in
  general: it can not be represented as the unfolding of a finite graph. Ho
 wever\, it can be represented as the result of the (infinite) evaluation o
 f a higher-order recursion scheme (HORS). If one wants to verify monadic s
 econd-order logic (MSO) formulas over such trace trees\, it means that the
 y have to be somehow lifted to the HORS. This is possible and leads to a d
 ecidable verification problem (Ong 2006).\n\nNow HORS are equivalent to si
 mply-typed lambda-terms with recursion. And this lamba-calculus admits sem
 antics and type systems. Kobayashi and Ong (2009) used a type system to re
 prove Ong's result. In 2015-2016\, Grellois and Melliès obtained another p
 roof using semantics\, in parallel with Salvati and Walukiewicz. The compl
 exity measure was refined in 2018 by Clairambault\, Grellois and Murawski.
 \n\nWe will in a first time explain this type-theoretic and semantic appro
 ach for the deterministic case\, and which contemporary research lines it 
 paves the way for.\n\nThe next challenge is to extend this deterministic c
 ase to the probabilistic case. We will quickly show results about terminat
 ion:\n- how to extend the lambda-calculus to a constrained probabilistic s
 etting\, and to obtain a decidable soundness result using companion one-co
 unter Markov decision processes (OC-MDPs) (Dal Lago-Grellois 2017\, 2019)
 \n- how to extend HORS to a probabilistic setting\, and what we can get of
  it (Kobayashi-Dal Lago-Grellois 2019\, 2020)\n\nThe talk will not require
  any prerequiste on lambda-calculi\, type systems or semantics.
DTSTART;TZID=Europe/Paris:20220214T150000
DTEND;TZID=Europe/Paris:20220214T160000
LOCATION:LaBRI - 178 - https://bordeaux-inp-fr.zoom.us/j/89508306159
SEQUENCE:0
SUMMARY:[MTV] Charles Grellois (LIS) - Verification of (probabilistic) func
 tional programs
TRANSP:OPAQUE
END:VEVENT
END:VCALENDAR
