Ningning

EvEff. Efficient Haskell effect handlers based on evidence translation.

GHC-Core-Literature-Review. Literature review of GHC's Core language, System FC

MpEff. Efficient effect handlers based on Evidence Passing Semantics.

Consistent-Subtyping-for-All. Haskell implementation and Coq proof for an implicit polymorphic gradual type system.

Dissertation. My PhD Thesis

dependent-types-in-haskell. Demo code for the talk Dependent Types in Haskell in Hong Kong Functional Programming meetup

Row-and-Bounded-via-Disjoint. Coq proof for elaborating row polymorphism and bounded polymorphism into disjoint polymorphism.

TypeInfer. Type inference for 'type level computation one step at a time'

haskell-programming-from-first-principles. Notes and Exercises for the book Haskell Programming from First Principles

type-driven-develop. Exercise Solution for the book Type Driven Development with Idris

haskell-trainings. Haskell 101 and 102: slides and codelabs

software_foundation_exercises. Exercises of book Software Foundation

xnning.github.io. HTML

FunImpl. Materials of the draft paper "Type-level Computation One Step at a Time"

dex-lang. Research language for array processing in the Haskell/ML family

vim-f2j-highlight. Highlight f2j code in Vim editor

hugo-academic. The website designer for Hugo. Build and deploy a beautiful website in minutes :rocket: