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:7027@i2m.univ-amu.fr
DTSTART;TZID=Europe/Paris:20190603T110000
DTEND;TZID=Europe/Paris:20190603T120000
DTSTAMP:20241120T202652Z
URL:https://www.i2m.univ-amu.fr/evenements/verification-of-probabilistic-f
 unctional-programs-charles-grellois/
SUMMARY:Charles Grellois (LIS\, LIRICA team\, Aix-Marseille Université): V
 erification of (probabilistic) functional programs - Charles Grellois
DESCRIPTION:Charles Grellois: There are several paradigms for programming l
 anguages\, among which functional programming\, which allows functions to 
 take other functions as input. For instance\, given a function f : Nat --&
 gt\; Nat mapping an integer to an integer\, and given a list of integers L
  = [i1\,i2\,...]\, we can define in functional programming the function ma
 p which maps the tuple (f\,L) to the integer list [f(i1)\,f(i2)\,...]. Thi
 s function map takes the function f as input.\nOur purpose is to verify pr
 operties of such programs. As we will see\, it is a challenging task\, bec
 ause the potential executions of these programs can not be conveniently re
 presented as finite graphs. They are rather described by higher-order recu
 rsion schemes\, which give a way to generate an infinite tree representing
  the behaviour of the program. Then\, we want to verify properties (from m
 onadic second order logic\, which contains the usual temporal logics LTL a
 nd CTL) over this infinite tree of behaviours. We will see that this is de
 cidable\, thanks to a variety of tools among which type theory.\nWe will t
 hen see a few ways to describe and analyze probabilistic functional progra
 ms\, and notably to address the probabilistic termination problem: how lik
 ely is it that a given program will terminate?\n
ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2
 020/01/Charles_Grellois.jpg
CATEGORIES:Séminaire,MABioS
END:VEVENT
BEGIN:VTIMEZONE
TZID:Europe/Paris
X-LIC-LOCATION:Europe/Paris
BEGIN:DAYLIGHT
DTSTART:20190331T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
END:DAYLIGHT
END:VTIMEZONE
END:VCALENDAR