Type Safety in 10 Easy, 4 Medium, and 1 Hard Lemma using Step-indexed Logical Relations
``` {-# OPTIONS --rewriting #-} module rewriting.examples.BlogTypeSafety10Easy4Med1Hard where open import Data.Bool using ( true...
Semantic Type Soundness and Language Interoperability
Notes by Amal Ahmed (OPLSS)