Run make to build. Tested with Coq 8.13.2.

Properties mentioned in the paper

• BoundIn: BoundVars.v
• Globally Unique Variables: UniqueBinders.v
• Well-scoped Expressions: WellScoped.v
• Pure Bindings: Purity.v

Translation relations mentioned in the paper

• Variable Renaming: Rename.v
• Inlining: Inline.v
• Beta redexes: Beta.v
• Splitting recursive let groups: SplitRec.v
• Unwrap-wrap elimination: Unwrap.v
• Dead-code elimination: DeadCode.v
• Let-floating: FloatLet.v
• Encoding of non-strict bindings: LetNonStrict.v
• Thunking of recursive bindings: ThunkRecursions.v
• Encoding of non-recursive bindings: LetNonRec.v
• Compatibility: Compat.v