personal page of Simon Cruanes

picture of me


I work at Aesthetic Integration in Austin, Texas, on Imandra, where I help write a user friendly, powerful proof system based on computational logic. I moved to Austin, Texas 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 (I'm applying for the board!); 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

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.



GNU/Linux and free software

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


Most of the programs I write and maintain nowadays are on my github profile; most are in OCaml. You can also take a look at the documentation of some of the libraries below (might be outdated).

Old scripts, hacks, and projects