• Stars
    star
    89
  • Rank 360,753 (Top 8 %)
  • Language
    OCaml
  • License
    MIT License
  • Created over 5 years ago
  • Updated about 2 years ago

Reviews

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

Repository Details

Experiment on how to bootstrap the OCaml compiler

More Repositories

1

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.
OCaml
86
star
2

PolyGen

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

pforth

A Forth implementation on a virtual machine ran by Python
Python
5
star
4

Mesecons_simulator

Python
4
star
5

itest

Lua
3
star
6

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/ )
OCaml
3
star
7

coq-proofs

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

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/ ).
Scala
2
star
9

prologin2015

My submission for the prologin2015 contest: http://www.prologin.org
OCaml
2
star
10

forth_computer

Computer for Minetest, programmable in Forth
Lua
2
star
11

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.
OCaml
1
star
12

technic_tutorial

Python
1
star
13

coq_hanoi

Formalisation of Hanoi towers in Coq
Coq
1
star
14

prologin2016

My submission for the prologin2016 contest: http://www.prologin.org
C++
1
star
15

foundations-of-proof-systems-project

Project for the "Foundation of proof systems" course of the MPRI.
Coq
1
star
16

wires

Lua
1
star