Personal page of Simon Cruanes


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 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; 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

Interesting links


Support Wikipedia

This page uses markdown, and GNU Make.

back to home

glider image