This is the web page of Ilias Garnier, researcher in computer science.

Personal information

I now work at Nomadic Labs in Paris on Tezos-related stuff.


dec 2018 - : Nomadic Labs (Paris)
april 2018 - nov 2018 : ENS Paris
aug 2017 - march 2018 : Sivienn
jan 2017 - jul 2017 : ENS Paris, Antique team, with Vincent Danos
sept 2014 - dec 2016 : Edin. U. and ENS Paris, Antique team, with Vincent Danos
2013 - sept 2014 : Edinburgh University, LFCS, Danos group
2012 - march 2013 : Edinburgh University, LFCS, CerCo project with Ian Stark
2012 : PhD (Paris Sud university, CEA LIST)
2008 : 2nd year graduation (MPRI master, Paris 7 university)
2007 : 1st year graduation (STIC master, Poitiers university)
1984 : birth (Poitiers, France)


I'm a computer scientist specialised in programming languages theory. Physics is nature's programming language, so I also like physics.
And everything in between.

Activities (except conference talks)

  • PC member, MFPS 2019
  • PC member, MFPS 2018
  • Talk given at the PIHOC workshop in Bologna
  • Talk given to the Department of Mathematics of Savoie University on Stoch. Mech. of Graph Rewriting (September 2016)
  • Talk given to the COMETE team at INRIA Saclay on Pointless Bayesian inversion (September 2016)
  • Talk given to Alexandra Silva's group at UCL on Giry and the Machine (April 2016)
  • Talk given at the Logic and Semantics seminar in Cambridge on Giry and the Machine (April 2016)
  • Talk given to the LACL, Paris-Est University on Giry and the Machine (April 2016)
  • Talk given to the COMETE team at INRIA Saclay on Giry and the Machine (March 2016)
  • Talk given at the LFCS seminar of U. Edinburgh on Dirichlet is Natural (December 2015)
  • Talk given to the Department of Mathematics of Savoie University on Dirichlet is Natural (November 2015)
  • I attended the ICTP Spring College on the Physics of Complex Systems in June 2014, Trieste. Fantastic teachers and gorgeous place.
  • PhD defended on February, 10 2012
  • I attended the Dagstuhl seminar on Game Semantics and Program Verification (June '10). A lot of fascinating talks. Thanks to the organizers !
  • Papers

    I'm in the process of making my papers publicly available. If you can't find a paper, please e-mail me and I'll send you a copy.


    The algebras of graph rewriting (with N. Behr, V. Danos and T. Heindel)
    Borel Kernels and their Approximation (with F. Dahlqvist, V. Danos and A. Silva)


    If you are curious about what I did during my Ph.D., you should learn French and then read the document.
    There's also an abstract in English, if you're lazy.
    My thesis

    Technical reports

    New Implementation of a Parallel Composition Primitive for a Functional BSP Language
    M2 report, under the supervision of Frederic Gava. 2008


    Mathematical structures of probabilistic programming
    PPS Workshop, co-located with POPL'17 (Paris). 2017

    On the Reaction Time of Some Synchronous Systems
    ICE Workshop, co-located with DisCoTec'11 (Reykjavik). 2011

    Formally Ensuring Time Constraints in a Development Process
    VVPS Workshop, co-located with ICAPS'11 (Freiburg). 2011

    New Implementation of a BSP Composition Primitive with Application to the Implementation of Algorithmic Skeletons
    APDCM Workshop, co-located with IPDPS'O9 (Rome). Joint work with Frederic Gava. 2009


    Continuous time Markov chains as transformers of unbounded observation functions (with V. Danos, T. Heindel and J. G. Simonsen)
    FOSSACS 2017

    Pointless learning (long version) (with F. Clerc, F. Dahlqvist and V. Danos)
    FOSSACS 2017

    Bayesian inversion by omega-complete cone duality (with F. Dahlqvist, V. Danos and O. Kammar)
    CONCUR 2016

    Robustly parameterised higher-order probabilistic models (with F. Dahlqvist and V. Danos)
    CONCUR 2016

    Stochastic Mechanics of Graph Rewriting (with N. Behr and V. Danos)
    LICS 2016

    Giry and the Machine (with F. Dahlqvist and V. Danos)
    MFPS 32, 2016

    Dirichlet is natural (with V. Danos)
    MFPS 31 (Nijmegen), 2015

    Sur le delai de separabilite dans des systemes synchrones
    MSR'11 (in French)


    Free energy of Petri nets (with V. Danos)
    Horizons of the Mind. A Tribute to Prakash Panangaden, 2014

    CPS Implementation of a BSP Composition Primitive with Application to the Implementation of Algorithmic Skeletons
    Parallel, Emergent and Distributed Systems, 2010

    Cool software

    I'm a happy user of OCaml and Linux.

    Not-so-cool software

    I have stripped myself of all shame in order to present my own creations to the world.
    For more recent stuff, take a look at my github.
    For oldish stuff:
  • mlphysics   A simple graphics engine, with a z-buffer based rendering pass and RGB texturing. Coded in OCaml, but I was still under the
    influence of C++ at the time. This is a port of a C++ physics engine which I never finished. Back in the day, I used a strange
    naming scheme, using suffixes to distinguish between local and global identifiers, and making the code unbearable. It compiles and runs, though.
  • lambda-pi   A parser and typechecker for a little dependently typed lambda-calculus based on LF. Everything is coded in OCaml, and the parsing
    depends on menhir. I planned to add inductive types, Dybjer-style, but my PhD got in the way.
  • MAO   MAO is a small unfinished compiler for the pure subset of core ML. It features polymorphic type inference, pattern matching compilation,
    monomorphisation, data type specialisation and various other passes. Its roots are in the programming project of the 2.4.2 course of the MPRI.
    The monomorphisation bit is issued from my work on BSML. I cleaned everything, implemented pattern matching and was finally too busy to implement
    the final pass (generating LLVM IR). The name is a reference to the STALIN Scheme optimising compiler, but since then another team stole my
    brillant idea for their own project.
  • Some domain theory in Coq   This is a small development I did in order to 1) learn domain theory 2) refresh my knowledge of Coq.
    It follows the plan of the first chapter of "Domains and Lambda-Calculi", by Amadio and Curien. I planned to prove the isomorphism
    between omega-algebraic DCPOs and the ideal completion of their compact elements but I did not finish it.
  • Parasite-mode for emacs and repetition-checker   Writing style does matter. When typing down large documents (e.g. a thesis), it is easy to
    repeat some words too often. Checking throughout the same text over and over again is tiresome: computers are designed for this kind of task.
    Sadly, my editor of choice (emacs) uses emacs-lisp as an extension language, and coding stuff in that language feels like a time-trip to the seventies.
    Thus, I coded the parasite-mode for emacs, which allows to run an external process, feeding it a file containing the text of the current buffer and
    receiving back emacs-lisp commands. As an example, I coded such a program (in OCaml) allowing to check word repetitions in an UTF-8 buffer, underlining
    them in emacs. All the heavy-duty work is done in OCaml, but the whole stuff is quite language-agnostic. To install it, you have to compile everything by
    yourself (there are on elisp file and one caml file). The caml file depends on extlib. Have fun.
  • The Rocinante Algol compiler   Rocinante is a small compiler for a lovecraftian variant of Algol.
    The language features variables, one-dimensional arrays, recursive functions and records to handle multiple arguments in a lazy way. Code generation relies
    on LLVM, through the OCaml bindings (in version 2.9). If I ever finish it, I plan to use it as a backend for a higher-level functional language (e.g. the one
    up there). For now, eveything is heap-allocated, and I plan to remedy this using a static analysis based on abstract interpretation. The analyser itself is
    there, relying on the Fixpoint library of B. Jeannet for all the solving part. Functions or arrays are not analysed for now. Functions should be easy, arrays
    a bit less, and representing the memory in a non-dumb way should present an interesting challenge. For now, it should at least be useful for people looking for
    examples of using LLVM and Fixpoint in OCaml. Note: relies on menhir for parsing, llvm-ocaml bindings v. 2.9 in /usr/lib/ocaml/llvm-2.9 (no symlink) and
    ocamlbuild for compilation. Might contain trace amounts of code by J.C. Filliatre.
    * update, rocinante christmas edition: bugfixes and a location-based heap memory model.
  • Everything up there is public domain, of course.
  • Cool links

  • Dictionnaire TLFi
  • Dictionnaires etymologiques pour un bon paquet de langues
  • Le cafard cosmique
  • Goodbye boredom

  • The excellent Olin Shivers' Hong-Kong files (that was before the retrocession)
  • YOUNG-HAE CHANG HEAVY INDUSTRIES: minimalist web-art, maximum impact
  • FAQ

    Q. Who is Lord Grandrith ?
    A. A pulp fiction hero invented by SF author P.J. Farmer in his novel "A Feast Unknown".
    This was a major inspiration to me, during my early childhood.