Encoded untyped lambda calculus in C++ template system! With type-to-string representation of terms and domain, the Y combinator works well :-)
Library for the SIP protocol in Ocaml.
CPS based compiler for functional language (deprecated by the Opifex project).
Compiler for MiniAlgol language, a mini-language with call-by-name, call-by-ref and call-by-value.
Skeleton for the RTS in Ocaml (in progress).
Proof search, based on focusing, for linear logic propositional calculus. Done with Wojciech Jedynak (wjzz)
Haskell bindings to GNU Aspell
Calculating derivative, step by step, for elementary functions (arcsin, sin, ...).
My academic attempt to formalize Completeness theorem for First Order Logic.
Portable user-level threading library for POSIX systems. Interface is similar to PTHREAD.