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

Personal information

I'm currently doing my Phd thesis at the CEA (French Atomic Energy Commission),
under the direction of Guy Vidal-Naquet and Christophe Aussagues. I primarily work
on formal methods applied to hard real-time embedded systems.

History

2008 : 2nd year graduation (MPRI master, Paris 7 university)
2007 : 1st year graduation (STIC master, Poitiers university)
1984 : birth (Poitiers, France)

Interests

I'm interested in programming languages (especially functional ones) and
their underlying theory and compilation, in parallel programming and more
broadly formal methods.

News

I attended the Dagstuhl seminar on Game Semantics and Program Verification (June '10). A lot of fascinating talks. Thanks to the organizers !

Papers

Technical reports

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

Workshops

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

Journals

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

Cool research

This section is devoted to things I'd like to understand in depth.

The work revolving around Epigram 2 is pretty neat. Observational type theory,
containers and all. The main advantage (from my unexperienced POV) of OTT is that
it allows to reason less intensionally than other intuitionistic type theories, therefore
permitting a clean integration of co-inductive reasoning. This kind of feature is of
utmost importance when formalising systems that don't stop, for instance nuclear plants and
pacemakers. Support for co-inductive predicates is in the existing tools quite brittle.
Confer :
  • Conor McBride
  • Thorsten Altenkirch
  • Neil Ghani

    • The Epigram 2 programming language will be based on these features:
  • Epigram website

    • In the same spirit, the work on "state-dependent IO-monad" is an interesting read.
  • Anton Setzer
  • Peter Hancock

    • Also, I found the work of Hancock and al. on "brouwerian stream processors" to be a nice read.

    Game semantics is another interesting body of work. The aim of game semantics is to give
    a syntax-free view of operational semantics. Two major results:
    full abstraction for PCF (i.e., game semantics allow to soundly and completly model
    sequential programming languages with higher-order functions), and decidability of the
    observational equivalence for a fragment of Algol, by means of a beautiful translation
    of the programs into equivalent regular expressions on the languages defined by the
    strategies. A good place to start:
  • Samson Abramsky
    • Another interesting fact is that this kind of semantics is very flexible, and readily
    extended to handle various programming constructs (parallelism, exceptions, non-determinism).

    There is a deep and well-known link between logic and computation at the root of type theories,
    which is called the "Curry-Howard-DeBruijn isomorphism". A few scientists seek to investigate this
    kind of analogy to other parts of science, more precisely theoretical physics and topology.
    By formalising all these domains using category theory, one sees that the underlying structure has some
    deep invariants. They form what is called "monoidal categories". A good introduction to the
    subject is the following paper:
  • Physics, Topology, Logic and Computation: A Rosetta Stone (John Baez)

    • Cool software

  • The Coq proof assistant
  • The Objective Caml language
  • TODO, blah blah

    • Cool links

  • Inspiration for the computer scientists of the new millenium
  • A lot of good learning material
  • MIT OpenCourseWare
  • Textfiles dot com , a well of pure entropy
  • Mathworld
  • FP and Type Theory
  • Category theory applied to functional programming applied to physics [...]
  • Programming language theory
  • Online Mandarin dictionary
  • Online Mandarin dictionary
  • Real-time ray-tracing board
  • Dictionnaire TLFi
  • Dictionnaires etymologiques pour un bon paquet de langues
  • Le cafard cosmique
  • Le Wub, guide des univers obliques

    • Goodbye boredom

  • The adventures of Cizia Zyke. Funny and trash. (in french)
  • 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.