Semantic typing for heap_lang
In this MR I define a semantic typing judgment for heap_lang, prove all the usual typing rules, safety, and semantic typing of the symbol table example from @dreyer's POPL talk.
Some interesting differences compared to the current logrel development:
- By building on top of heap_lang, we get the nice notations and tactics from heap_lang for free. No more De Bruijn for expressions!
- I only defined semantic types, not syntactic types. One could define syntactic types in the future and prove the fundamental theorem, but I was not too interested in doing that.
- Due to the value restriction, we need to thunk
∀types. I thus model the type-level abstraction
λ: <>, eand the type level application
- Due to step-indexing, we need to take a step to prove the typing rule for unfolding recursive types. I defined the unfold operator
(λ: "x", "x") e.
- By having only semantic types, I could use Coq's binders in ∀ and ∃ types, and have nice notations. So, no more De Bruijn for types either.
- I defined a type
ltyas a record containing a predicate over values and a prove that the predicate is persistent. Notably, I used this record in the interpretation of ∀ and ∃ types, and thus no longer have to explicitly require the type to be persistent.
Typing judgment and typing rules
- I defined the semantic typing judgment
Γ ⊨ e : Aas an
iPropand stated all of the typing rules using
- I used type classes for operator typing (
LTyBinOp) and to keep track of unboxed types (