This is the web page of Ilias Garnier, researcher in computer science.
I now work at Nomadic Labs in Paris on Tezos-related stuff.
- ilias [dot] gar [at] gmail [dot] com
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 !
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.
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)
Pointless learning (long version) (with F. Clerc, F. Dahlqvist and V. Danos)
Bayesian inversion by omega-complete cone duality (with F. Dahlqvist, V. Danos and O. Kammar)
Robustly parameterised higher-order probabilistic models (with F. Dahlqvist and V. Danos)
Stochastic Mechanics of Graph Rewriting (with N. Behr and V. Danos)
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
I'm a happy user of OCaml and Linux.
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.
Dictionnaires etymologiques pour un bon paquet de langues
Le cafard cosmique
The excellent Olin Shivers' Hong-Kong files (that was before the retrocession)
YOUNG-HAE CHANG HEAVY INDUSTRIES: minimalist web-art, maximum impact
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.