Details on GitHub


Intro: Hadrian is a new build system for the Glasgow Haskell Compiler. It is based on Shake and we hope that it will eventually replace the current make-based build system.

Contributions: Dynamic linking, installation rules, cross compilation etc.


Intro: a library with examples built in Coq, based on Iris framework. This is the artifact of my Bachelor's thesis: "An Extensible Verification Framework for Higher-Order Concurrent Imperative Programs".


Intro: Iris is a Higher-Order Concurrent Separation Logic Framework implemented and verified in the proof assistant Coq.

Contributions: Atomicity related verification, ticket lock etc.


Intro: The Haskell Lightweight Virtual Machine (HaLVM): GHC running on Xen. It is one example of Unikernel and is created and maintained by Galois Inc.

Contributions: Porting HaLVM-GHC from v7.8 to v8.0; Integration of the HaLFS file system library


Intro: Servo is a modern, high-performance browser engine written in Rust language. It is created by Mozilla Research, and being built by a global community, from individual contributors to companies such as Mozilla and Samsung.

Contributions: Implementation of File etc. DOM APIs and resource backends


Intro: PureScript is a small strongly typed programming language that compiles to JavaScript. The infrastructure is written in Haskell and it is in many ways like Haskell.

Contributions: PSCi REPL refactoring and libraries patches

Also some old projects...


JavaScript API misuese checking based on the eXtended WebIDL specification, including (highly) experimental integration with TAJS and SAFE analyzers.


A library targeting at providing high-level, extensible, easy to use Haskell interface to Z3 solver.


RuScript is an experimental object-oriented language. The project includes two parts: rvm (RuScript Virtual Machine) written in Rust and rusc (RuScript Compiler) written in Haskell.


JavaScript static analyzer, an experimental hack


"BBQ" is derived from name of a project by my friend, and "SG" means static-page generator. It is something similar to Jekyll. it is written in Haskell and maintained as a library. Here is also a scaffolding site


Hackern is the codename for my OS course project. It is a series of efforts in building infrastructure for HaLVM unikernel.

Updated in: April 2017

Back to home