Hello!

I am a Research Software Engineer at Lean FRO, working on the Lean theorem prover. My research interests span automated reasoning, formal semantics, and verification, with a particular focus on coinductive methods in computer science. Alongside my industrial role, I maintain active ties with academia as an Academic Visitor in the Department of Mathematics at Imperial College London and an Industrial Academic Visitor in the Department of Computer Science and Technology at the University of Cambridge.

I earned my PhD in Computer Science from University College London, under the supervision of Alexandra Silva, as part of the Programming Principles, Logic and Verification Group. During my doctoral studies, I completed two research internships with the Automated Reasoning Group of Amazon Web Services in Seattle.

I hold a BSc in Computer Science from the University of Southampton, where I was supervised by Julian Rathke. I have also undertaken internships with the Software and Large Scale Systems Group at ARM Research in Cambridge, and at Goldman Sachs in London.

Outside of work, I enjoy shooting analog photography, drinking coffee, and collecting vinyl records from around the world.

You can reach me at #eval (fun name => name ++ "@lean-fro.org") "wojciech" or ping me at Linkedin.

Research

Talks

Teaching