# 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:

### Expressions

- 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`Λ e`

as`λ: <>, e`

and the type level application`e _`

as`e #()`

. - Due to step-indexing, we need to take a step to prove the typing rule for unfolding recursive types. I defined the unfold operator
`rec_unfold e`

as`(λ: "x", "x") e`

.

### Types

- 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
`lty`

as 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 : A`

as an`iProp`

and stated all of the typing rules using`-∗`

. - I used type classes for operator typing (
`LTyUnOp`

,`LTyBinOp`

) and to keep track of unboxed types (`LTyUnboxed`

).

Edited by Robbert Krebbers