Skip to content

Semantic typing for heap_lang

Robbert Krebbers requested to merge robbert/logrel_heaplang into master

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 Λ 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.


  • 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).

CC @amintimany @dfrumin @dreyer

Edited by Robbert Krebbers

Merge request reports