Toggle navigation
Jianba Blog
Home
About
Archive
Archive
keep hungry keep foolish
Show All
46
笔记
36
Coq
36
SF (软件基础)
36
PLF (编程语言基础)
19
LF (逻辑基础)
16
C#
3
数据结构
1
生活
1
经典排序
1
.net core
1
C++
1
CS Idols
1
Meta
1
Mysql
1
QC (Quickcheck)
1
jwt
1
mysql
1
2020
.net core控制台程序链接Mysql
.net core控制台程序链接Mysql
基于.net core3.1的JWT授权01
基于.net core3.1的JWT授权01
C#笔记
C#笔记
Mysql
十大经典排序
C++指针和地址
C++指针和地址
2019
Git基础命令
快速搭建Hexo博客
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
2015
Hello 2015
"Hello World, Hello Blog"