Sergei Romanenko

spsc. SPSC: A Small Positive Supercompiler

agda-simple-scp. A simple supercompiler formally verified in Agda

staged-mrsc-agda. Staged multi-result supercompilation (a model in Agda)

agda-samples. A collection of samples in Agda

spsc-scala. A Small Positive Supercompiler in Scala

agda-Pythagoras. Pythagorean theorem (sqrt 2 is not rational). Rewritten in Agda2 from the original proof by Thierry Coquand.

agda-miscellanea. Experiments with Agda

agda-Ramsey-theorem. Intuitionistic Ramsey theorem (a proof in Agda)

agda-almost-full. Almost-full relations: an Agda version for "Stop when you are almost-full"

chapman-big-step-normalization. Big-step normalization (formalized in Agda)

agda-hsubst-revised. Hereditary substitutions for simple types (revised)

spinalhdl-samples. Some experiments with SpinalHDL

spsc-idris. A Small Positive Supercompiler in Idris

unmix. A simple program specializer (based on partial evaluation) for a subset of Scheme. It includes a binding time analyzer, a residual program generator and an arity raiser. Imported from Google Code.

scp-notes-ru. Notes on supercompilation (in Russian). The sources for the site

sat4j-experiments. Experiments with Sat4j.

agda-Higman-lemma. Constructive proofs of Higman’s lemma formalized in Agda

idris-norm-by-traversals. Traversal-based normalization for ULC

idris-samples. A collection of samples in Idris

mrsct. A variation of mrsc based on traits + self-types

sergei-romanenko.github.io. The sources for the site

mrsc-trs. Domain-specific supercompilation for transition systems (based on the MRSC toolkit).

agda-normalization. Normalization by evaluation and big-step normalization formalized in Agda

staged-mrsc-idris2. Staged multi-result supercompilation (in Idris2)

chapman-normalization-delay-monad. Normalization by evaluation in the delay monad (formalized in Agda)

julia-samples. Jupyter Notebook