Archive

2025-03-13-申请南方电网和银行模版

申请南方电网和银行模版

2025-03-12-申请亲青公寓

申请亲青公寓

2025-03-11-处理完遗留的事项

处理完遗留的事项

2025-03-10-面试

面试做测评

2025-03-09-周日

周日好像已经不像周末了，而是周一的前一天

2025-03-08-JAVA周六

新的休息日

2025-03-07-招聘会周五

好累啊，真是不想填了

2025-03-06-招聘会

2025-03-06-招聘会

2025-03-05-通宵投简历

2025-03-05-通宵投简历

2025-03-04-复习更新

2025-03-04-复习更新

2025-03-03-复习国网

2025-03-03-复习国网

2025-03-02-准备小银行春招

2025-03-02-准备小银行春招

2025-03-01-春招大爆发

2025-03-01-春招大爆发

20250228随笔_三大运营商投完

20250228随笔_三大运营商投完

20250227随笔_0124到0206春招投完

20250227随笔_0124到0206春招投完

20250226随笔_春招工作+找平信

20250226随笔_找工作

20250225随笔_信银申请+国网+医保

20250224随笔_resume+国网+医保

20250223随笔_只投了一个兴业银行

20250221随笔_活下去

太累，别思考了

博客还有什么作用

"思考"

申请信银GBA信用卡

"思考"

信银国际大湾区双币信用卡开卡及使用

信银国际大湾区双币信用卡开卡及使用

20250219图床

"图床搭建成功，哈哈哈哈"

如何绑定自己的博客域名

"永久免费哦"

2025-02-19-永久免费图床搭建

"永久免费哦"

探索 Markdown 的奇妙世界

"探索 Markdown 的奇妙世界"

永久免费图床搭建

记录一下日常生活吧

"Hello World, Hello 2025"

git,github和vscode

"Hello World, Hello 2025"

首篇博客的诞生

"Hello World, Hello 2025"

Data Representation - Floating Point Numbers

「数据表示」浮点数

Data Representation - Integer

「数据表示」整数

My Programming Languages Spectrum

我的编程语言光谱

「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