The HTML page of S. A. Mimram

CEA Saclay Nano-INNOV
Institut CARNOT CEA LIST
DILS/LMEASI
Point Courrier 174
91191 Gif sur Yvette CEDEX, France

Phone: +33 1 69 08 00 09

Samuel Mimram
samuel.mimram@ens-lyon.org

I have done my PhD thesis in the PPS team and I am now working in the MeASI team at CEA Saclay. You can have a look at my curriculum vitæ.

Research interests

Denotational semantics (game semantics in particular), concurrency, rewriting theory, category theory, linear logic, programming languages, algebraic topology, hybrid systems.

Publications

Asynchronous Game semantics

From Asynchronous Games to Concurrent Games with Paul-André Melliès, unpublished manuscript.
Focusing in Asynchronous Games, invited presentation at the 6th conference on Computability In Europe (CIE'10), in proceedings, LNCS volume 6158, pages 331-341, 2010 (arXiv, HAL, presentation).
Asynchronous Games: Innocence without Alternation with Paul-André Melliès, 18^th International Conference on Concurrency Theory (CONCUR'07), volume 4703 of LNCS, pages 395-411, 2007 (arXiv, HAL).
Innocence asynchrone, master thesis report (slides).

Higher-dimensional rewriting theory

Towards Higher-Dimensional Rewriting Theory, submitted.
Representing 2-Dimensional Critical Pairs, unpublished manuscript.
The Structure of First-Order Causality (extended version), Mathematical Structures in Computer Science 21 (01), pages 65-110, 2011. (arXiv, HAL)
Computing Critical Pairs in 2-Dimensional Rewriting Systems, in proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), pages 226-242, 2010 (arXiv, HAL, presentation).
The Structure of First-Order Causality, 24^th Symposium on Logic in Computer Science (LICS'09), in proceedings, pages 212-221, 2009 (arXiv, HAL, presentation).

Models for concurrency

Trace Spaces: an Efficient New Technique for State-Space Reduction with Lisbeth Fajstrup, Éric Goubault, Emmanuel Haucourt and Martin Raussen, accepted at ESOP'12.
Rigorous evidence of freedom from concurrency faults in industrial control software, with Richard Bonichon, Géraud Canet, Loïc Correnson, Éric Goubault, Emmanuel Haucourt, Michel Hirschowitz and Sébastien Labbé, in proceedings of SAFECOMP 2011, LNCS 6894, pages 85-98, 2011.
Formal Relationships Between Geometrical and Classical Models for Concurrency, with Eric Goubault, submitted (arXiv, HAL).

Hybrid systems

A Non-Standard Semantics for Kahn Networks in Continuous Time with Romain Beauxis, accepted at CSL'11 (arXiv, HAL, slides).

Webradios

Liquidsoap: a High-Level Programming Language for Multimedia Streaming, in proceedings of SOFSEM 2011, pages 99-110, 2011.
De la webradio lambda à la λ-webradio with David Baelde, Journées Francophones des Langages Applicatifs (JFLA'08), in proceedings, pages 47-62, 2008 (HAL).

PhD thesis

My PhD thesis Sémantique des jeux asynchrones et réécriture 2-dimensionnelle (TEL) with its presentation.

Presentations

Guaranteed Topological Methods for Dynamical Systems, séminaire LMeASI, 25 January 2012.
Towards Efficient Computation of Trace Spaces of Concurrent Programs, séminaire, Orsay, 18 November 2011.
A Non-Standard Model for Kahn Networks in Continuous Time, Séminaire PPS, Paris, 15 November 2011.
Towards Efficient Computation of Trace Spaces of Concurrent Programs, Workshop on Computational Topology, Toroto, Canada, 8 November 2011.
Critical Pairs in 2-Dimensional Rewriting Systems, Operads and Rewriting, Lyon, 3 November 2011.
Towards Efficient Computation of Trace Spaces of Concurrent Programs, workshop CHOCO, Lyon, 4 April 2011.
Algebraic Tools in Game Semantics, GT Jeux, 26 october 2010.
Cubical Sets and Petri Nets: an Adjunction, workshop on Geometric and Topological Methods in Computer Science (GETCO'10), 11 january 2010.
A Local View on Innocence, workshop in Roma, 24 April 2009.
Jeux et Sémantique : journée Théorie des Jeux et Informatique, 18 février 2009.
De la webradio lambda à la λ-webradio : groupe de travail programmation de PPS, 20 novembre 2008.
Présentation d'une sémantique de jeux pour la quantification du premier ordre : réunion de l'ANR INVAL, 25 septembre 2008.
Ma présentation du 1^er avril 2008 à l'EJCIM intitulée Une sémantique de jeux asynchrone pour la logique linéaire.
Ma présentation du 20 décembre 2007 à la réunion de l'ANR CHOCO intitulée Innocence dans les sémantiques de jeux asynchrones.
Ma présentation du 7 septembre 2007 à la conférence CONCUR 2007 intitulée Asynchronous Games: Innocence without Alternation.
Ma présentation au groupe de travail concurrence du 21 juin 2007 intitulée Asynchronous Games: Innocence without Alternation.
La présentation (et mes notes) que j'ai faite à la rencontre GÉOCAL du 30 octobre 2006, à Lyon, sur Une théorie algébrique de la sémantique des jeux.
La présentation que j'ai donnée au séminaire thésards le 15 mars 2006 sur l'innocence asynchrone et non alternée.
La présentation (et mes notes) que j'ai faite à la rencontre GÉOCAL du 24 février 2006 au CIRM, à Luminy sur l'innocence non alternée.
Ma présentation sur l'innocence asynchrone à la rencontre GÉOCAL du 20 juin 2005.

Enseignements

Les TD de λ-calcul et catégories donnés au MPRI.
La page de mes enseignements.
Des TDs de caml que j'ai donné en sup.

Stages

Mon rapport de stage de 2^e année sur la décidabilité de l'égalité dans les catégories avec familles à l'Université de Chalmers à Göteborg (en Suède) sous la direction de Thierry Coquand et les slides de ma présentation (un bon exemple de ce qu'il faut faire pour se ramasser sur une présentation).
Un rapport sur JoCaml et le join-calcul ainsi que les transparents de la présentation pour le cours de DEA de mobilité.
Mon rapport de stage MIM₁ sur la recherche automatique de preuves dans une logique spatiale sur le π-calcul (stage de permière année effectué au LIP, à l'ÉNS Lyon, sous la direction de messieurs Daniel Hirschkoff et Étienne Lozes). Et voici les slides de la soutenance.
Des documents pour les ptits MIMs.
Divers documents que j'ai écrits en prépa (fiches, TIPE, etc.).

Prog

Savonet est un générateur de streams musicaux permettant de faire une radio par le web (il est capable de maintenir une base de donnée des fichiers musicaux disponibles, de gérer des règles de programmation évoluées et est doté d'une interface web, telnet et irc pour que les auditeurs puissent interagir en temps réel avec la radio). J'en maintiens des packages Debian de la nouvelle version.
An OCaml binding to OpenCL. This version is still preliminary, comments are very welcome.
strid, a string diagram generator.
ocaml-glpk, une librarie caml qui est un binding de GLPK.
Funk, un petit noyau programmé en caml (si si c'est possible !).
motocal, un petit programme ocaml pour synchroniser mon calendrier Evolution et mon téléphone portable Motorola.
Le patch ocaml-memprof pour étudier la consommation mémoire des programmes caml (cf. le readme) mis à jour pour OCaml 3.10.0 (et OCaml 3.09.3). Ce patch a été créé par Fabrice Le Fessant, je n'ai fait que le mettre à jour pour les versions récentes d'OCaml.
Bed, un éditeur de texte qui tente de s'acquiter efficacement de sa tâche (l'indentation en particulier).
gkrellm-cpuspeed un plugin gkrellm qui affiche la vitesse du processeur en se fondant sur /proc/cpu (contrairement à gkrellm-x86info qui recalcule cette vitesse ce qui donne des résultats moins probants sur mon ordi avec speedstep).
irc.ml (le mli et la doc correspondants), un joli petit module Caml pour faire des clients (ou des bots) IRC. Celui-ci a servi de base à camlquizz, un bot pour faire des quizz sur IRC (allez voir le canal #superquizz de irc.rezosup.org).
skeg, un projet images dont le but est d'animer un pingouin en metaballs en utilisant des techniques de cinématique inverse.
bifton est un compilateur d'un sous-ensemble de Pascal en assembleur i386 et sparc écrit en caml.
Roudoudou est un éditeur de partitions graphique en frontend pour lilypond (qui est lui-même un éditeur de partitions fondé sur LaTeX) programmé en Java (POOGL en MIM₁). Il est loin d'être en version finale, ni même en version β, ni même d'être utilisable étant donné que la syntaxe de lilypond a quelque peu évolué depuis la version 2.0.0…
Un interpréteur lisp programmé en OCaml dont je doute qu'il puisse un jour servir à qu[o]i que ce soit (second DM de MIM₁). Il contient quelques erreurs importantes de conception, bien cachées…
Fractcompr est un programme permettant de compresser des images par compression fractale écrit en OCaml (premier DM de MIM₁).
J'essaie aussi de maintenir des packages Debian.

Misc

My CV.
My public keys: ssh and gpg.
Les partitions de la fantaisie et fugue en sol mineur bwv 542 de Bach (ou en midi) que je soumettrai un jour à Mutopia quand j'aurai le courage de finir tout ça (fut une époque où je savais moi-même écrire des machins comme ça).