sergei-romanenko Goto Github PK

agda-almost-full

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

agda-higman-lemma

Constructive proofs of Higman’s lemma formalized in Agda

agda-hsubst-revised

Hereditary substitutions for simple types (revised)

agda-kripke-models

Continuation-passing style Kripke models

agda-miscellanea

Experiments with Agda

agda-normalization

Normalization by evaluation and big-step normalization formalized in 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

chapman-big-step-normalization

Big-step normalization (formalized in Agda)

chapman-normalization-delay-monad

Normalization by evaluation in the delay monad (formalized in Agda)

chisel3-samples

Some experiments with Chisel3

cilpe

Automatically exported from code.google.com/p/cilpe

diff-zoo-romanenko

Differentiation for Hackers

halide-hls

HLS branch of Halide

hosc-docs

HOSC documentation exported from code.google.com/p/hosc. The sources for the site

idris-norm-by-traversals

Traversal-based normalization for ULC

idris-samples

A collection of samples in Idris

idris2-higman-lemma

Constructive proofs of Higman’s lemma formalized in Idris 2

idris2-pythagoras

Pythagorean theorem (sqrt 2 is not rational). Rewritten in Idris 2 from the original proof by Thierry Coquand.

idris2-samples

A collection of samples in Idris 2

jsai-romanenko

Clone of JSAI static analysis framework

julia-samples

markdown-test

A markdown test.

mrsc-trs

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

mrsct

A variation of mrsc based on traits + self-types

openacc-samples

Sample projects in OpenACC

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.

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.