Alexander Gryzlov

I am a research programmer at IMDEA Software Institute, working with Niki Vazou.

I specialize in programming language theory, formal verification & mechanized reasoning (including type systems, program logics, symbolic computation, and automated solvers) and their application in both systems programming (concurrency, distributed computing, cryptography, compilers, theorem provers, computer algebra) and computational modeling (probabilistic programming, economics, hybrid systems, bioinformatics). On the mathematical side, I prefer schools of thought that focus on compositionality and mechanization, such as constructive/synthetic mathematics, type theory, and category theory.

Currently I work on extending and maintaining LiquidHaskell, a liquid type-based system for automated reasoning about purely functional programs. I also co-maintain FCSL, FCSL-PCM and HTT projects, all of which are related to separation logic, a formalism for reasoning about stateful programs.

Contact

• twitter: clayrat
• linkedin: alexgryzlov
• telegram: @clayrat

Recent posts

• Three Lectures on Dialogues - June 2, 2025
• Program Analysis with Interpolants (and the history of model checking) - April 22, 2025
• Contemporary C++ - March 26, 2025
• Leveraging Program Analysis for Type Inference - October 22, 2024
• FDSA in SSReflect - October 10, 2024
• Cayley graphs (and ML) - August 14, 2024
• Structural abstract interpretation - July 23, 2024
• Quotient Haskell - February 10, 2024
• Programming and Proving with Guarded Recursion @ PSSV'23 - November 24, 2023
• Subtyping Without Reduction - August 25, 2023
• A Hoare logic style refinement types formalisation - August 17, 2023
• Propositional interpolation in SSReflect - July 24, 2023
• Swierstra's Hoare monad in SSReflect - June 14, 2023
• Propositional resolution in SSReflect - April 28, 2023
• Pointfree topology and constructive mathematics - April 13, 2023

…or you can find more in the archives.