Avatar

Lélio Brun

Postdoctoral research engineer in Computer Science

École normale supérieure

Inria

Biography

I am a postdoctoral research engineer in the Parkas team of the Computer Science department (DI) at École normale supérieure in Paris. I recently defended my thesis, Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset, written under the supervision of Marc Pouzet and Timothy Bourke.

I currently work on the verified compilation of Lustre, a synchronous language, through the proof assistant Coq.

Interests

  • Functional programming
  • Synchronous languages
  • Proof assistants

Education

  • PhD in Computer Science, 2020

    École normale supérieure - PSL Research University

  • MSc in Computer Science (MPRI), 2016

    Université de Paris

  • MSc in Aerospace Engineering, 2013

    ISAE-ENSMA

Projects

Vélus

A prototype compiler for Lustre, verified in Coq.

Obelisk

A tool to pretty-print (e.g., $\LaTeX$) Menhir grammars.

Experience

 
 
 
 
 

Postdoctoral research engineer

École normale supérieure / Inria – PARKAS Team

Jan 2020 – Present Paris, France
 
 
 
 
 

Software engineer

Astek

May 2014 – Aug 2014 Le Plessis Robinson, France

Teaching

Teaching assistant

Academic service

Contact

  • lelio.brun@inria.fr
  • École normale supérieure, DI, PARKAS
    45 rue d'Ulm
    75230 cedex 05 Paris
  • Walk around the right side of the main building, take the sliding door that gives access to the DI, take the staircase at right down one level and then turn left and then right.
  • Chat on Keybase