Séminaire, 17 janvier 2013

Lieu

La rencontre aura lieu à l'École Normale Supérieure de Lyon, campus Jacques Monod, en amphi C le matin, amphi B l'après-midi. Pour venir, voir les instructions sur le site du LIP ou sur un plan, par exemple chez Google Maps. À l'entrée, se présenter à la réception, qui aura la liste des inscrits.

Programme

10:30 – 12:00
Michele Pagani (Univ. Paris 13)
Invited talk: Syntax vs Semantics: a quantitative bridge

Since its inception, various models of Linear Logic have been defined in categories of vector spaces (more generally modules) and linear functions. These models provide semantics of quite expressive higher-order functional programming languages, where the denotation of a program is given by a matrix.

A natural question then arises -- What is the computational meaning of the scalars appearing in such matrices?, Can we recover from them some operational behavior that is hidden in the standard (domain based) semantics?

Danos & Ehrhard give a first positive answer in the specific case of probabilistic coherence spaces. We address the question in a more general setting, providing a general construction of adequate models parametrized by a continuous semiring of scalars. We show how specific instances of such a semiring allow to compare programs not only with respect to "what they can do", but also in "how many steps" or "with what resources" or in "how many ways" (for non-determistic calculi) or "with what probability" (for probabilistic calculi).

(This is a joint work with Jim Laird (Bath), Giulio Manzonetto (Paris 13) and Guy McCusker (Bath))

14:00 – 15:00
Alastair F. Donaldson (Imperial College, London)
Invited talk: GPUVerify: a Verifier for GPU Kernels

I will describe GPUVerify, a collaboration between Imperial College London and Microsoft Research Redmond on the design and implementation of a technique and tool for analysing concurrent software written to run on graphics processing units (GPUs). GPUVerify checks the kernel functions that execute across cores of a GPU architecture and attempts to detect, or verify absence of, two kinds of defects: data races and barrier divergence. To scale to large numbers of threads, GPUVerify exploits the relatively simple nature of the GPU programming model in a way that allows verification of massively parallel kernels to be reduced to a sequential program verification task. In this talk I will describe the defects that GPUVerify checks for, present some details of the verification technique, and discuss open problems in this area.

This is joint work with:

  • Adam Betts, Nathan Chong, Peter Collingbourne*, Jeroen Ketema, Paul Thomson (Imperial)

  • Shaz Qadeer (Microsoft)

    (*) now at Google

15:30 – 16:30
Barbara Petit (Inria Rhône-Alpes)
Invited talk: Geometry of types