Archive

keep hungry keep foolish
2020

Data Representation - Floating Point Numbers

「数据表示」浮点数

Data Representation - TODO

「数据表示」待写

Data Representation - Integer

「数据表示」整数

My Programming Languages Spectrum

我的编程语言光谱

2019

Peter John Landin

「计算机科学偶像」- 彼得·约翰·兰丁

My Spacemacs Workflow

From Vim to Spacemacs

把「终端下的 Vim」作为 macOS Finder 的打开方式

Open file with terminal Vim from the macOS Finder

「SF-QC」2 TypeClasses

Quickcheck - A Tutorial on Typeclasses in Coq

「SF-PLF」19 PE

Programming Language Foundations - Partial Evaluation

「SF-PLF」18 UseAuto

Programming Language Foundations - Theory And Practice Of Automation In Coq Proofs

「SF-PLF」17 UseTactics

Programming Language Foundations - Tactic Library For Coq

「SF-PLF」16 LibTactics

Programming Language Foundations - A Collection of Handy General-Purpose Tactics

「SF-PLF」15 Norm

Programming Language Foundations - Normalization of STLC

「SF-PLF」14 RecordSub

Programming Language Foundations - Subtyping with Records

「SF-PLF」13 References

Programming Language Foundations - Typing Mutable References

「SF-PLF」12 Records

Programming Language Foundations - Adding Records To STLC

「SF-PLF」11. TypeChecking

Programming Language Foundations - A Typechecker for STLC

「SF-PLF」10 Sub

Programming Language Foundations - Subtyping (子类型化)

「SF-PLF」9 MoreStlc

Programming Language Foundations - More on The Simply Typed Lambda-Calculus

「SF-PLF」8 StlcProp

Programming Language Foundations - Properties of STLC

「SF-PLF」7 Stlc

Programming Language Foundations - The Simply Typed Lambda-Calculus

「SF-PLF」6 Types

Programming Language Foundations - Type Systems

「SF-PLF」5 Smallstep

Programming Language Foundations - Small-Step Operational Semantics

「SF-PLF」4 HoareAsLogic

Programming Language Foundations - Hoare Logic as a Logic

「SF-PLF」3 Hoare2

Programming Language Foundations - Hoare Logic, Part II

「SF-PLF」2 Hoare

Programming Language Foundations - Hoare Logic, Part I

「SF-PLF」1 Equiv

Programming Language Foundations - Program Equivalence (程序的等价关系)

「SF-LC」16 Auto

Logical Foundations - More Automation

「SF-LC」15 Extraction

Logical Foundations - Extracting ML From Coq

「SF-LC」14 ImpCEvalFun

Logical Foundations - An Evaluation Function For Imp

「SF-LC」13 ImpParser

Logical Foundations - Lexing And Parsing In Coq

「SF-LC」12 Imp

Logical Foundations - Simple Imperative Programs

「SF-LC」11 Rel

Logical Foundations - Properties of Relations

「SF-LC」10 IndPrinciples

Logical Foundations - Induction Principles

「SF-LC」9 ProofObjects

Logical Foundations - The Curry-Howard Correspondence

「SF-LC」8 Maps

Logical Foundations - Total and Partial Maps

「SF-LC」7 Ind Prop

Logical Foundations - Inductively Defined Propositions (归纳定义命题)

「SF-LC」6 Logic

Logical Foundations - Logic in Coq

「SF-LC」5 Tactics

Logical Foundations - More Basic Tactics

「SF-LC」4 Poly

Logical Foundations - Polymorphism and Higher-Order Functions

「SF-LC」3 List

Logical Foundations - Working with Structured Data

「SF-LC」2 Induction

Logical Foundations - Proof by Induction

「SF-LC」1 Basics

Logical Foundations - Functional Programming in Coq

2018

Vim 与中文输入法

Using Vim with non-english input method

Avoiding success at all cost

Watching "Escape from the Ivory Tower: The Haskell Journey"

程序员中的梦想家

Dreamers among programmers

2017

「知乎」如何通俗地解释停机问题？

How to explain the Halting Problem?

「知乎」如何证明不可计算的函数比可计算的函数多？

Why is there more uncomputable functions?

「知乎」为什么 CSS 这么难学？

Why I dislike CSS as a programming language

Farewell, Flash. 感谢你，但这一次是真正的永别。

So long, and thanks for all the Flash

饿了么的 PWA 升级实践

Upgrading Ele.me to Progressive Web App

How does SW-Precache works?

「知乎」如何理解 document 对象是 HTMLDocument 的实例？

Why is document an instance of HTMLDocument?

下一代 Web 应用模型 —— Progressive Web App

The Next Generation Application Model For The Web - Progressive Web App

如何客观地评价「小程序」的体验?

Wechat Mini-Program vs. the Web, a UX comparison

2016

Service Worker 101「GDG DevFest 2016 北京」

🎞 Slides:Service Worker 101, Working Offline and Instant Loading (GDG DevFest 2016 Beijing)

Progressive Web Apps，复兴序章「QCon 上海 2016」

🎞 Slides:Progressive Web Apps, Make Web Great Again. (QCon Shanghai 2016)

Web 在继续离我们远去

After the release of Wechat Mini-Program

Progressive Web App 之我见

🎞 Slides:Progressive Web App, in my points of view

「译」React vs Angular 2：冰与火之歌

React versus Angular 2: There Will Be Blood

2015

都 2015 年了，CSS 怎么还是这么糟糕

🎞 Slides:CSS Still Sucks 2015

「译」iOS 9，为前端世界都带来了些什么？

iOS 9, Safari and the Web: 3D Touch, new Responsive Web Design, Native integration and HTML5 APIs

「知乎」设计师如何学习前端？

How designers learn front-end development?

「译」ES5, ES6, ES2016, ES.Next: JavaScript 的版本是怎么回事？

ES5, ES6, ES2016, ES.Next: What's going on with JavaScript versioning?

JavaScript 模块化七日谈

🎞 Slides:JavaScript Modularization Journey

聊聊「阿里旅行 · 去啊」—— 行业与战略

聊聊在线旅行行业与老东家的产品思路

JavaScript Module Loader

CommonJS，RequireJS，SeaJS 归纳笔记

See you, Alibaba

再见，阿里。

hUX 随想录（二）：操作系统的浪漫主义 —— Metro 篇

信息、载体、抽象、UI 设计乱谈

Unix/Linux 扫盲笔记

不适合人类阅读，非常水的自我笔记

Definition of End to End User Scenarios

hUX 随想录（一）：Digital native 数字原住民

两岁的侄女天天叫着手机手机

「知乎」如何评价 2015 年 3 月 9 日 Apple 春季发布会？

聊聊科技与新式奢侈品

Hello 2015

"Hello World, Hello Blog"

2014

「知乎」如何看待微信屏蔽快的打车事件？

恰有小感。

「知乎」你们觉得响应式好呢，还是手机和PC端分开来写？

「知乎」为什么阿里系软件体验都不好？

或许这就是所谓的企业 DNA

「知乎」对中国用户而言，Pure Android 是否比 MIUI 或 Flyme 体验更好？

「知乎」如何评价 MIUI 6？