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
- Wojciech Różowski, “Completeness Theorems for Behavioural Distances and Equivalences”, Doctoral thesis (Ph.D), UCL (University College London) [UCL theses repository]
- Gabriele Lobbia, Wojciech Różowski, Ralph Sarkis, Fabio Zanasi, “Quantitative Monoidal Algebra: Axiomatising Distance with String Diagrams” - [arxiv preprint] (Accepted to MFCS 2025)
- Spencer van Koevering, Wojciech Różowski, Alexandra Silva, “Weighted GKAT: Completeness and Complexity” [arxiv preprint] (Accepted to ICALP 2025)
- Stefan Zetzsche, Wojciech Różowski, “Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny” - [full paper] (Accepted to ICTAC 2024)
- Keri D’Angelo, Sebastian Gurke, Johanna Maria Kirss, Barbara König, Matina Najafi, Wojciech Różowski, Paul Wild, “Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques” - [arxiv preprint] (Accepted to CONCUR 2024)
- Wojciech Różowski, “A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions” - [arxiv preprint] (Accepted to ICALP 2024)
- Wojciech Różowski and Alexandra Silva, “A Completeness Theorem for Probabilistic Regular Expressions” - [arxiv preprint] (Accepted to LICS 2024)
- Wojciech Różowski, Tobias Kappé, Dexter Kozen, Todd Schmid and Alexandra Silva, “Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity” - [arxiv preprint] (Accepted to ICALP 2023)
- Todd Schmid, Wojciech Różowski, Alexandra Silva and Jurriaan Rot, “Processes Parametrised by an Algebraic Theory” - [arxiv preprint] (Accepted to ICALP 2022)
- Wojciech Różowski, “Formally verified derivation of an executable and terminating CEK machine from call-by-value λp̂-calculus” - [Extended abstract] (Accepted to ICALP 2021 Student Research Competition)
Talks
- Lean Together 2026 - Online - January 2026 - video
- Dafny 2025 @ POPL - Denver - January 2025 - video 1, video 2
- 4th Southern and Midlands Logic Seminar - Birmingham - December 2023 - slides
- ICALP’23 - Paderborn - July 2023 - slides
- Research visit at Barbara König’s group - Duisburg - July 2023 - slides
- Adjoint School Seminar (joint talk with Johanna Maria Kirss and Matina Najafi)- Online - April 2023 - slides
- Cornell Programming Languages Discussion Group - Ithaca - February 2023
- The Workshop on Verification of Probabilistic Programs - Haifa - August 2022 - slides
- Midlands Graduate School in Foundations of Computer Science - Nottingham - April 2022 - slides
- Programming Principles, Logic and Verification Group Seminar - London - January 2022 - slides
Teaching
- Assistant for Theory of Computation- UCL - Semester 2 - 2023/2024
- Assistant for Mathematics and Statistics - UCL - Semester 2 - 2023/2024
- Assistant for Intermediate Mathematics for Computer Science - UCL - Semester 2 - 2022/2023
- Assistant for Computability and Complexity Theory - UCL - Semester 1 - 2022/2023
- Assistant for Logic and Database Theory - UCL - Semester 1 - 2022/2023
- Assistant for Mathematics and Statistics - UCL - Semester 2 - 2021/2022
- Assistant for Logic and Database Theory - UCL - Semester 1 - 2021/2022
