「SF-PLF」6 Types
This chapter: typing relation — 定型关系 type preservation ...
「SF-PLF」7 Stlc
this chapter: (change to new syntax…) function abstraction variable binding — 变量绑定 substitution ...
「SF-PLF」8 StlcProp
基本的定理依赖关系 top-down: Type Safety Progress Canonical Forms (one for each type of value) Preservati ...
「SF-PLF」9 MoreStlc
make the STLC into a PL! Simple Extensions to STLC 其实这一部分我好像没有任何必要做笔记…… NumbersSee StlcProp.v exe ...
「SF-PLF」10 Sub
ConceptsThe Subsumption RuleThe Subtype RelationSlide QA1Record Subtyping… row type index? record i ...
「SF-PLF」11. TypeChecking
The has_type relation is good but doesn’t give us a executable algorithm — 不是一个算法but it’s syntax di ...
「SF-PLF」12 Records
Adding Records123456789101112t ::= Terms: | {i1=t1, ..., in=tn} ...
「SF-PLF」13 References
Hux: this chapter is very similar to TAPL - ch13 ReferencesBut under a “formal verification” concep ...
津公网安备 12011002021027号