Toggle navigation
JinGuang Blog
Home
About
Archive
Archive
keep hungry keep foolish
Show All
44
笔记
39
Coq
36
SF (软件基础)
36
PLF (编程语言基础)
19
LF (逻辑基础)
16
基础
3
C
3
C++
3
Vim
3
CS Idols
1
Emacs
1
QC (Quickcheck)
1
2021
My Spacemacs Workflow
From Vim to Spacemacs
Vim 与中文输入法
Using Vim with non-english input method
把「终端下的 Vim」作为 macOS Finder 的打开方式
Open file with terminal Vim from the macOS Finder
2020
Data Representation - Floating Point Numbers
「数据表示」浮点数
Data Representation - TODO
「数据表示」待写
Data Representation - Integer
「数据表示」整数
My Programming Languages Spectrum
我的编程语言光谱
2019
Peter John Landin
「计算机科学偶像」- 彼得·约翰·兰丁
「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
