My Home Page at Keldysh Institute of Applied Mathematics.
-
My GitHub profile.
-
A number of proofs formalized in Agda:
- A simple supercompiler formally verified in Agda.
- Staged multi-result supercompilation: a model in Agda and an implementation in Scala (without proofs).
- Almost-full relations: an Agda version for "Stop when you are almost-full".
- Intuitionistic Ramsey Theorem.
- Constructive proofs of Higman’s lemma implemented in Agda.
- Hereditary substitutions for simple types (revised).
- A collection of samples in Agda.
-
SPSC: A Small Positive Supercompiler in Scala, Haskell, Python, Ruby & JavaScript.
-
Unmix, a program specializer (based on partial evaluation) for a subset of Scheme. See also a version for Racket by Danil Annenkov.
-
Notes on supercompilation (in Russian).