Project Page
Index
Table of Contents
PR.base
PR.contexts
Types
Environment structure
Environment simplification
PR.reduction
Single-step reduction
Multi-step reduction
PR.stlc
Instantiation
Identity instantiation
Composition of instantiations
Automation
PR.sn_defs
Strong normalization
PR.sn_inductive_2a
PR.sn_inductive_2b
Logical Relation
PR.sn_inductive_soundness_1a
Different Characterisations Strong Normalisation
Closure Properties of sn
PR.sn_inductive_soundness_1b