Le 14 octobre à la FRUMAM – de 9h30 à 12h30.
Orateur : Ugo Dal Lago (UniBo)
Titre : On Higher-Order Cryptography
Résumé : Type-two constructions abound in cryptography: adversaries for encryption and authentication schemes, if active, are modeled as algorithms having access to oracles, i.e. as second-order algorithms. But how about making cryptographic schemes higher-order themselves? Moreover, how about seeing cryptographic reductions as higher-order functions? We give an answer to this question, by first describing why higher-order cryptography is interesting as an object of study, and then showing how the concept of probabilistic polynomial time algorithm can be generalised so as to encompass algorithms of order strictly higher than two. We then prove some positive and negative results about the existence of higher-order cryptographic primitives, namely authentication schemes and pseudorandom functions. The talk is based on some joint work with Boaz Barak and Raphaëlle Crubillé.
Orateur : Pierre Clairambault (LIS)
Titre : Games with no Winner: an Introduction to Game Semantics
Résumé : How to define rigorously the behaviour of programs under execution?
Program semantics is a necessary first step in order to prove that a program or program transformation is correct, and is of course a preliminary to any theoretical question on programming languages. Game semantics is one of many approaches to program semantics. It represents a program by recording the exchange of observable computational events with its execution environment, phrased as a play in a two-player game that the program plays with its context. In game semantics there is no winner: it is about the journey, not the destination!
Most of my talk will be an introduction to game semantics. I will first focus on some old (but nice) results, namely the so-called « semantic cube » following which game semantics exactly captures the observable behaviour of programs with various computational effects (notably, mutable state and non-local control). I will show how this allows one to prove results about computational effects and their interferences.
Time permitting, I will then talk about some of my own recent work on a game semantics for concurrent programs. The semantics builds on so-called « true concurrency » models such as event structures, and provides a causal description of the behaviour of concurrent programs with rich computational features.
Orateur : Raphaelle Crubillé (LORIA)
Titre : Sémantique dénotationelle pour les languages de programmation probabilistes
Résumé : La sémantique dénotationelle est un champs de recherche centré sur la construction de modèles mathématiques des languages de programmation, visant à produire des techniques de preuve pour l’équivalence de programmes. Dans les dix dernières années, l’usage des probabilités pour la programmation a été transformé par les dévelopements en programmation statistique et en apprentissage, ce qui a stimulé un intérêt renouvelé pour les méthodes formelles pour des languages probabilistes. Cet exposé présente un bref panorama de la sémantique dénotationelle des langages de programmation probabilistes, en tentant d’expliciter à la fois ses enjeux, ses outils et ses perspectives.