Certified NBE procedure for the Martin-Lof type theory -- my master thesis (in progress).
Prototype for simple garbage collector
Library for pretty printing.
Our solution for ICFP2013, done with
Impala Operating System - The UNIX-like system. My bechelor's project, done in 2009 with two friends -- shm and takeshi. Kernel supports VM, VFAT(MEMFS, FAT12), ISA DMA, Floppy controller, Sun Slab Allocator, threads. User-space contains zlib, ash, tar, vttest, our libpthread, our libc!
Ocaml manpage renderer
Extraction of the untyped lambda evaluator in Coq
Simple TCP/IP HTTP server in amd64 assembler.