Rémy_Citérin

Intermediate
@RemyCiterin

DijkstraMonad. formalization of Dijkstra Monad using "Dijkstra Monads for All" from Kenji Maillard et al. 2019

11

AdventOfFPGA. Bluespec

9

Superscalar. A superscalar RISCV core in bluespec

5

rust-gcode. A work-in-progress implementation of gcode writer for the CNC of hackens

4

LeanCoInd. definition of coinductives types (M-types and indexed M-types) in Lean4, and some utilities for reasoning

4

CoIndStar. implementation of ocinductive datatypes and interaction trees in FStar

3

Spacer. reimplementation of a part of the Spacer model checker using Z3 and OCaml

3

RedPitaya. test of the red pitaya board with yosys and nextpnr

3

SeparationLogic. Lean

3

zig-scheduler. a work in progress scheduler for zig using work stealing with Chase-Lev deque

2

fstar-experiments. multiples expérimentations autours du langage F*

2

LeanCat. toy implementation of category in Lean4

2

ArduinoStar. F*

2

DOoOM. DOoOM Out-Of-Order Machine

2

BlueTileLink. Implementation of the TileLink bus protocol in Bluespec

2

nixos-config. Nix

1

bram-bug-yosys-nextpnr-xilinx. Verilog

1

nexys-video. Some experiments on my new Nexys Video board using Yosys+Nextpnr

1

ZigSAT. A work in progress SAT solver write in Zig

1

RayTracingBluespec. Ray Tracing in One Weekend in Bluespec System Verilog

1

jax-rl. Python

1

compiler-experiments. A compiler experimentation playground in rust

1

MiniLustre. OCaml

1

3DRiscV. Some experimentations with the blarney DSL for hardware synthesis

1

jax-experiments. Python

1

xv6-rv32. Port of MIT's xv6 OS to 32 bit RISC V

1
26
Apply