Evènement pour le groupe Séminaire Méthodes Formelles


Date 2019-11-05  07:00-07:00
TitreProgrammation temps réel et concurrente avec flux monadique / Concurrent and realtime programming with monad streams 
RésuméRésumé : A priori, on ne peut pas faire du temps réel avec un langage fonctionnel générique (OCaml, Haskell). Les raisons de cet apriori sont nombreuses: ces langages sont trop lents, ils usent d’un ramasse miette, etc… pire encore avec Haskell qui est paresseux. A posteriori, en étant ni le premier ni le dernier, j’y arrive. Pour cela, je définis la notion de flux monadique, c’est à dire un type de listes dont l’accès est (inductivement) gardé par une action monadique. Dans cette exposé je me propose de: - expliquer cette notion centrale en programmation fonctionnelle typée de programmation monadique, - de montrer comment définir le type des flux monadiques, qui peuvent être utilisé, selon le cas, comme entrée ou sortie, - d’étendre la programmation monadique à la programmation concurrente à l’aide de références monadique, - de montrer combiner tous ça en un mélange de programmation synchrone (pour le traitement des flux audio) et de programmation asynchrone (pour le contrôle de ces traitements), - d’illustrer ça par l’exemple, en temps réel, in situ. Pour ceux qui se posent la question, l’API résultante produit des programmes sans deadlock (PAS BESOIN DE VERIFIER QUOIQUE CE SOIT). Asbtract : A priori, realtime programing cannot be achieved with generic typed functional programing language such as OCaml or Haskell. Reasons for this are numerous : these languages are slow, they have a garbage collector, and, even worse for Haskell, it is lazy. A posteriori, and I’m neither the first nor the last, this is possible. For such a purpose, I define and use a notion of monad stream, that is, lists where accessing elements is (inductively) guarded by a monadic action. In this talks, I shall: - describe this central notion of monad programing in functional typed programing, - show how monad streams are defined and encode both input and output streams, - extend the notion of monad action to monad action reference for concurrent programming, - show (and prove) how all this can be used for synchronous processing (audio transform) and asynchronous control (transform parameterization), - illustrate all this by live realtime and concurrent experiments … in Haskell… For those who might ask, the resulting API is deadlock free by construction… (NO VERIFICATION NEEDED) 
Lieu178 
OrateurDavid Janin 
Emailhttps://www.labri.fr/perso/janin/ 
UrlLaBRI 



Aucun document lié à cet événement.

Retour
Retour à l'index