Wojciech K. Różowski

Wojciech K. Różowski

PhD candidate at UCL

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.

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, learning foreign languages, and collecting vinyl records from around the world.

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

News

  • August 2025 - My thesis corrections have been approved, and I have officially been awarded my doctorate!
  • July 2025 - Passed my PhD viva with minor corrections! My examiners were Filippo Bonchi and Clemens Kupke.
  • June 2025 - Consider submitting an extended abstract to BMQL2025, where I am honoured to serve as a PC member this year.
  • August 2024 - “Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny” got accepted for publication at ICTAC 2024.
  • July 2024 - “Behavioural Metrics: Compositionality of the Kantorovich Lifting and an Application to Up-To Techniques” got accepted to CONCUR 2024.
  • June 2024 - Started an another summer intenship at at Automated Reasoning Group of Amazon Web Services in Seattle.
  • May 2024 - two of my papers got accepted! One at LICS and one at ICALP.
  • January 2023 - Passed my transfer viva! Also, Stefan Zetzsche and I wrote a blog post about formalising bialgebraic semantics of regular expressions using Dafny and its fantastic support for coinductive reasoning.
  • August 2023 - Started my internship at Automated Reasoning Group of Amazon Web Services in Seattle.
  • April 2023 - My paper “Probabilistic Guarded KAT Modulo Bisimilarity: Completeness and Complexity” (joint work with Tobias Kappé, Dexter Kozen, Todd Schmid and Alexandra Silva) was accepted to ICALP!
  • February 2023 - Got accepted for Adjoint School 2023 to a “Behavioural Metrics, Quantitative Logics and Coalgebras” project!
  • January 2023 - Visiting Cornell University.

Research

Talks

Teaching