Projects

Details on GitHub

Hadrian

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.

Iris-C

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".

Iris

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.

HaLVM

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

Servo

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

PureScript

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...

xWIDL

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

z3-encoding

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

RuScript

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.

Dynamic

JavaScript static analyzer, an experimental hack

BBQ-SG

"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

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