Charles Grellois
LIS, LIRICA team, Aix-Marseille Université
http://research.grellois.fr/
Date(s) : 03/06/2019 iCal
11 h 00 min - 12 h 00 min
There are several paradigms for programming languages, among which functional programming, which allows functions to take other functions as input. For instance, given a function f : Nat –> Nat mapping an integer to an integer, and given a list of integers L = [i1,i2,…], we can define in functional programming the function map which maps the tuple (f,L) to the integer list [f(i1),f(i2),…]. This function map takes the function f as input.
Our purpose is to verify properties of such programs. As we will see, it is a challenging task, because the potential executions of these programs can not be conveniently represented as finite graphs. They are rather described by higher-order recursion schemes, which give a way to generate an infinite tree representing the behaviour of the program. Then, we want to verify properties (from monadic second order logic, which contains the usual temporal logics LTL and CTL) over this infinite tree of behaviours. We will see that this is decidable, thanks to a variety of tools among which type theory.
We will then see a few ways to describe and analyze probabilistic functional programs, and notably to address the probabilistic termination problem: how likely is it that a given program will terminate?
Catégories