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/spsc
SPSC: A Small Positive Supercompiler
sergei-romanenko/staged-mrsc-agda
Staged multi-result supercompilation (a model in Agda)
sergei-romanenko/spsc-scala
A Small Positive Supercompiler in Scala
sergei-romanenko/agda-Pythagoras
Pythagorean theorem (sqrt 2 is not rational). Rewritten in Agda2 from the original proof by Thierry Coquand.
sergei-romanenko/spinalhdl-samples
Some experiments with SpinalHDL
sergei-romanenko/spsc-idris
A Small Positive Supercompiler in Idris
sergei-romanenko/agda-Higman-lemma
Constructive proofs of Higman’s lemma formalized in Agda
sergei-romanenko/mrsct
A variation of mrsc based on traits + self-types
sergei-romanenko/sergei-romanenko.github.io
The sources for the site
sergei-romanenko/staged-mrsc-idris2
Staged multi-result supercompilation (in Idris2)
sergei-romanenko/chisel3-samples
Some experiments with Chisel3
sergei-romanenko/diff-zoo-romanenko
Differentiation for Hackers
sergei-romanenko/Halide-HLS
HLS branch of Halide
sergei-romanenko/idris2-Higman-lemma
Constructive proofs of Higman’s lemma formalized in Idris 2
sergei-romanenko/idris2-Pythagoras
Pythagorean theorem (sqrt 2 is not rational). Rewritten in Idris 2 from the original proof by Thierry Coquand.
sergei-romanenko/idris2-samples
A collection of samples in Idris 2
sergei-romanenko/jsai-romanenko
Clone of JSAI static analysis framework
sergei-romanenko/julia-samples
sergei-romanenko/openacc-samples
Sample projects in OpenACC
sergei-romanenko/QuantumComputing
This is an implementation of IBM's Quantum Experience in simulation; a 5-qubit quantum computer with a limited set of gates. Please cite me if you end up using this academically.
sergei-romanenko/rigel
Rigel is a language for describing image processing hardware embedded in Lua. Rigel can compile to Verilog hardware designs for Xilinx FPGAs, and also can compile to fast x86 test code using Terra.
sergei-romanenko/SATExperiments.jl
Julia - Experiments with SAT solvers
sergei-romanenko/sc-mini
SC Mini is a "minimal" positive supercompiler
sergei-romanenko/sc-mini-scala
sc-mini: A Minimalistic Supercompiler written in Scala
sergei-romanenko/scala-lms-samples
Experiments with Scala LMS
sergei-romanenko/scsc-romanenko
sergei-romanenko/staged-mrsc-python
Staged multi-result supercompilation (in Python)
sergei-romanenko/staged-mrsc-rust
sergei-romanenko/staged-mrsc-scala
Staged multi-result supercompilation (in Scala)
sergei-romanenko/StagedMRSC.jl