Overview

• Module systems use dependent types.
• Type checking for dependent types is undecidable in the presence of non-terminating programs.
• Classical solution: Syntactic distinction between module language and core language.
• Modern approach: Semantic distinction via a synthetic phase distinction (Sterling and Harper’s ModTT).
• Contribution 1: Re-casting synthetic phase distinction in language of SOGATs.
• Contribution 2: Hippogriff, a small but non-trivial language showing that normalization by evaluation can be adapted for the synthetic phase distinction in a simple way.