
Modal Logic and Modal Types

Programming as Theory Building

Referential transparency, definiteness and unfoldability

When Encapsulation is a Sin

Synchronous Dataflow Programming Languages

Encoding Tuples and Variants in System F

Intuitionistic Logic

Dependent Type Theory and Interactive Theorem Prover

DSL  The bridge between productivity and performance

朱光潜《谈美》

Types and Programming Languages

Flow Control and Congestion Control in TCP

How to Setup Private Tor Network

Distributed Algorithms

Bound Variables and Lambda Calculus

WaitFree Concurrent Computing

读《东坡传》

Two fallacies of software product design

Different ways to calculate fibonacci numbers

A Better Architecture for 12306.cn