Boris Djalal

I am pursuing a PhD funded by Microsoft Research Inria Joint Centre in MARELLE, INRIA.

I have a penchant for minimalistic approaches and fields where one can acquire absolutely certain pieces of knowledge. My interests include fields which straddle mathematics and computer science, particulary formal proof - which helps us trust systems; practical mechanisms to enhance trust and governance.

I collaborated with Cyril Cohen on the formalization of Newton representation of polynomials, which resulted in my first research publication, at CPP 2016 conference. The code, upon which the publication is based can be downloaded from our github repository.

I formalized first order formulas in real closed fields and their geometric operations with Coq, which resulted in my second research publication, at CPP 2018 conference. This paves the way for the formalization of cylindrical algebraic decomposition. It can also be used to formalize mathematical analysis results in a constructive way.

This work is considerably eased thanks to SSReflect tactics and (broadly) Mathematical Components library.

The list of my publications is available on HAL.