Toggle navigation
putao Blog
Home
About
Archive
Archive
「我干了什么 究竟拿了时间换了什么」
Show All
61
笔记
38
Coq
36
SF (软件基础)
36
PLF (编程语言基础)
19
LF (逻辑基础)
16
Meta
9
知乎
4
Web
4
产品
2
基础
2
网络
2
C
2
C++
2
UX/UI
2
opcode
2
计算理论
1
译
1
CSS
1
JavaScript
1
PWA
1
QC (Quickcheck)
1
React
1
Slides
1
bond
1
code
1
daima
1
linux
1
2025
Bug使用
时间
"Hello World, Hello Blog"
BUG
"Hello World, Hello Blog"
2025-11-09更新
"Hello World, Hello Blog"
Video 11
heyue-2025
"Hello World, Hello Blog"
gen-2025
"Hello World, Hello Blog"
2024
图片动态
"Hello World, Hello Blog"
图片动态
"Hello World, Hello Blog"
Daima 2024
分区网络调试代码
🎞 Slides:Progressive Web App, in my points of view
分区网络交换机调试过程
详细步骤
分区网络交换机调试过程
详细步骤
操作代码?
2020
作为一个前端,看不懂@黄玄 的几乎每一个回答,只有我自己吗?
Taking this chance to reflect on myself
Data Representation - Floating Point Numbers
「数据表示」浮点数
Data Representation - Integer
「数据表示」整数
My Programming Languages Spectrum
我的编程语言光谱
React Hooks 是否可以改为用类似 Vue 3 Composition API 的方式实现?
Thinking in React vs. Thinking in Vue
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
2017
如何通俗地解释停机问题?
How to explain the Halting Problem?
为什么 CSS 这么难学?
Why I dislike CSS as a programming language
下一代 Web 应用模型 —— Progressive Web App
The Next Generation Application Model For The Web - Progressive Web App
2016
「译」React vs Angular 2:冰与火之歌
React versus Angular 2: There Will Be Blood
2015
Hello 2015
"Hello World, Hello Blog"
2014
Redhat创建bond?