Archive

【女权造谣系列】女权作了哪些恶？中文互联网的女权造谣现状。

是谁在制造厌男狂欢？

【女权造谣系列1】被掩盖的女性家暴者

【女权造谣系列3】别再装瞎！数据撕碎"性侵=女性专属"的伪善遮羞布

【女权造谣系列4】某些人开始用谣言攻击儿童了吗？

【女权造谣系列9】为什么女权不是平权？浅谈女本位主义

Data Representation - Floating Point Numbers

「数据表示」浮点数

Data Representation - Integer

「数据表示」整数

My Programming Languages Spectrum

我的编程语言光谱

「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