Pinned Repositories
agda-almost-full
Almost-full relations: an Agda version for "Stop when you are almost-full"
agda-miscellanea
Experiments with Agda
agda-Pythagoras
Pythagorean theorem (sqrt 2 is not rational). Rewritten in Agda2 from the original proof by Thierry Coquand.
agda-Ramsey-theorem
Intuitionistic Ramsey theorem (a proof in Agda)
agda-samples
A collection of samples in Agda
agda-simple-scp
A simple supercompiler formally verified in Agda
spsc
SPSC: A Small Positive Supercompiler
spsc-scala
A Small Positive Supercompiler in Scala
staged-mrsc-agda
Staged multi-result supercompilation (a model in Agda)
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.
sergei-romanenko's Repositories
sergei-romanenko/agda-simple-scp
A simple supercompiler formally verified in Agda
sergei-romanenko/agda-samples
A collection of samples in Agda
sergei-romanenko/agda-miscellanea
Experiments with Agda
sergei-romanenko/agda-Ramsey-theorem
Intuitionistic Ramsey theorem (a proof in Agda)
sergei-romanenko/agda-almost-full
Almost-full relations: an Agda version for "Stop when you are almost-full"
sergei-romanenko/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.
sergei-romanenko/chapman-big-step-normalization
Big-step normalization (formalized in Agda)
sergei-romanenko/idris-norm-by-traversals
Traversal-based normalization for ULC
sergei-romanenko/idris-samples
A collection of samples in Idris
sergei-romanenko/mrsc-trs
Domain-specific supercompilation for transition systems (based on the MRSC toolkit).
sergei-romanenko/sat4j-experiments
Experiments with Sat4j.
sergei-romanenko/scp-notes-ru
Notes on supercompilation (in Russian). The sources for the site
sergei-romanenko/agda-hsubst-revised
Hereditary substitutions for simple types (revised)
sergei-romanenko/agda-normalization
Normalization by evaluation and big-step normalization formalized in Agda
sergei-romanenko/chapman-normalization-delay-monad
Normalization by evaluation in the delay monad (formalized in Agda)
sergei-romanenko/agda-kripke-models
Continuation-passing style Kripke models
sergei-romanenko/cilpe
Automatically exported from code.google.com/p/cilpe
sergei-romanenko/hosc-docs
HOSC documentation exported from code.google.com/p/hosc. The sources for the site
sergei-romanenko/markdown-test
A markdown test.
sergei-romanenko/zeno
Zeno