Ekdohibs/coq-proofs

Stars
3
Rank 3,963,521 (Top 79 %)
Language Coq
License
MIT License
Created almost 10 years ago
Updated almost 3 years ago

Ekdohibs/coq-proofs

Ekdohibs

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Various proofs in Coq. Contains the proof of quadratic reciprocity and of Baire theorem.

camlboot

Experiment on how to bootstrap the OCaml compiler

joujou

A compiler from a small functional language to C. Especially features algebraic effects and handlers with multishot continuations, and a static type system with inference of types and effects, with subtyping.

PolyGen

PolyGen is a code generator for the polyhedral model, written and proved in Coq.

pforth

A Forth implementation on a virtual machine ran by Python

Mesecons_simulator

itest

toy-smt

Toy SMT solver, for deciding SAT with equality theroy. Written for the Sémantique et applications à la vérification course at ENS ( https://www.di.ens.fr/~rival/semverif-2016/ )

pscala

Compiler from a fragment of Scala to x86-64 assembly. Was written for the Compilation course at ENS ( https://www.lri.fr/~filliatr/ens/compil/2015-2016/ ).

prologin2015

My submission for the prologin2015 contest: http://www.prologin.org

forth_computer

Computer for Minetest, programmable in Forth

netlist-simulator

Netlist simulator for the "Digital systems" course at ENS ( http://www.di.ens.fr/~bourke/sysdig.html ). Compiles netlist to C, with some optimizations.

technic_tutorial

coq_hanoi

Formalisation of Hanoi towers in Coq

prologin2016

My submission for the prologin2016 contest: http://www.prologin.org

wires

foundations-of-proof-systems-project

Project for the "Foundation of proof systems" course of the MPRI.

chamelon