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