Archive

「我干了什么 究竟拿了时间换了什么」
2023

2023年度总结


博客搭建指南


2021

《JavaScript 二十年》推荐语


2020

Data Representation - Floating Point Numbers

「数据表示」浮点数


Data Representation - Integer

「数据表示」整数


My Programming Languages Spectrum

我的编程语言光谱


2019

「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