《Java编程方法论 响应式之Rxjava篇》序在《2019 一月的InfoQ 架构和设计趋势报告》[^1]中，响应式编程（Reactive Programming）和函数式（Functional Programing）仍旧编列在第一季度（Q1）的 ...

This chapter: typing relation – 定型关系 type preservation and progress (i.e. soundn...

基本的定理依赖关系 top-down: Type Safety Progress Canonical Forms (one for each type of value) Preservation Substituion Context In...

ConceptsThe Subsumption RuleThe Subtype RelationSlide QA1Record Subtyping… row type index? record impl as list width/de...

this chapter: (change to new syntax…) function abstraction variable binding – 变量绑定 substitution – 替换 Overview“Base Ty...

make the STLC into a PL! Simple Extensions to STLC 其实这一部分我好像没有任何必要做笔记…… NumbersSee StlcProp.v exercise stlc_arith. Let Bin...

The has_type relation is good but doesn’t give us a executable algorithm – 不是一个算法but it’s syntax directed, just one typing r...

Adding Records123456789101112t ::= Terms: | {i1=t1, ..., in=tn} record | t.i...

Hux: this chapter is very similar to TAPL - ch13 ReferencesBut under a “formal verification” concept, it’s more interesting ...

1234Inductive ty : Type := (* record types *) | RNil : ty | RCons : string → ty → ty → ty. we need typecon to identify re...