sergei-romanenko.github.io

Sergei A. Romanenko’s GitHub Home Page

My Home Page at Keldysh Institute of Applied Mathematics.

My GitHub sites and projects

• 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.

• HOSC: A Higher-Order Supercompiler in Scala.

• 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).