Toggle navigation
小星星也变奏
Home
About
Archive
Archive
「我干了什么 究竟拿了时间换了什么」
Show All
42
笔记
38
Coq
36
SF (软件基础)
36
PLF (编程语言基础)
19
LF (逻辑基础)
16
基础
2
C
2
C++
2
JavaScript
1
QC (Quickcheck)
1
Web
1
annualReport
1
tutor
1
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