Personal page of Simon Cruanes

picture of me


I work at Imandra in the USA, where I help develop a user friendly, powerful proof system based on computational logic. I started in January 2018.

Previously (2015-10 to 2017-10) I was at Inria Nancy doing a postdoc with Jasmin Blanchette on a counter-example finder for higher order logic, nunchaku.

I completed my PhD after 3 years at Deducteam (INRIA), from October 2012 to September 2015, under the supervision of Gilles Dowek and Guillaume Burel. My work takes place in the field of first-order automated deduction. My thesis is titled "Extending Superposition with Integer Arithmetic, Structural Induction, and Beyond" and can be found below.

Before the PhD, I was a student in École polytechnique, in France, where I obtained an engineering diploma in 2012, then at EPFL, in Switzerland, where I got a master degree in Computer Science.

I am interested in Artificial Intelligence, formal logic, programming languages; swing dancing with the Austin Swing Syndicate; classical music and opéra, science-fiction and more generally by reading.

I used to be a member of the Binet Réseau, an association in charge of the students' network in École polytechnique.

Computer science

Other pages on this site

Publications and documents

My dblp page makes a better job than me at tracking my academic papers. Some of them can also be found on HAL.


My CV is here.



GNU/Linux and free software

I am using several GNU/Linux distributions, currently debian and archlinux. See this page.


Most of the programs I wrote (and, for some of them, maintain) are on my github profile; most are in OCaml.

Old scripts, hacks, and projects

(very old stuff)


Some links