Homepage

Hi! My name is André Duarte and I’m currently a software developer at IMC Trading, a high‑frequency trading firm in Amsterdam. I work all across the software stack: from Jupyter notebooks and Kafka data pipelines, down to chasing nanoseconds in high-performance distributed systems, or integrating custom hardware into critical trading loops.

I previously completed a PhD on automated theorem proving at the University of Manchester, under the supervision of Prof. Konstantin Korovin. I focused on efficient ways of dealing with specific hard theories, such as arithmetic or associative-commutative operators, while retaining the full completeness and generality of automated logical deduction for arbitrary problems. My research has applications in domains where these theories are important, such as in formal verification of software, or in theorem proving for mathematics.

Previously I got my BSc and MSc in Physics from the University of Coimbra, with a specialisation in computational physics, having written my thesis on the internal composition of neutron stars.

Feel free to reach out to me with any questions!

Contact me

  • mail [ɑt] andrepd.eu

For encryption, feel free to use this key.

If you’d like to reach me in some other way, please email me and I’ll be glad to exchange some other method of contact.

CV

Download my CV here.

Publications

See also my dblp and orcid pages.

Other stuff

  • quantum-tptp: Automated verification of quantum circuits.

  • ocaml-posit: A library for using Type III unums in OCaml. (WIP)

  • rprover: An automated theorem prover focusing on extensibility and speed, written in Rust.

  • LibriVox: My LibriVox contributions.