Léon Gondelman's Home Page



I am a post-doc researcher at iCIS in Nijmegen, Netherlands. I am member of Sovereign project, developping methods and tools for the verification of life-critical or safety-critical systems.

Currently, I am working on formalization of C language in Coq proof assistant using a higher-order concurrent separation logic framework called Iris.

I defended my PhD in December 2016 under supervision of Jean-Christophe Filliâtre and Andrei Paskevich at Université Paris Saclay in France.

My PhD thesis entitled "A Pragmatic Type System for Deductive Verification" explores solutions that a type system based approach can bring to the deductive verification. It formalizes some aspects of the type system of Why3 such as ghost code and static control of aliases.


  • main research topics :
    • program logics, deductive software verification
    • type systems and static analysis
    • functional programming
    • homotopy type theory, higher inductive types
  • lists of my publications


  • I am teaching assistant for a course on finite automata at Radboud University
  • During three years of my PhD, I was a teaching assistant for bachelor and master courses of functional programming, compilation, and logics.

Contact information:

  • Email: leon dot gondelman at gmail dot com
  • Office: 01.01, Mercator 1 building, Toernooiveld 212, Nijmegen 6525 EC