Project Page
Index
Table of Contents
Rec.Base.ARS
Abstract Reduction Systems
Rec.Base.axioms
Axiomatic Assumptions
Functional Extensionality
Propositional Extensionality
Rec.Base.fintype
Finite Types and Mappings
Forward Function Composition
Finite Types
Rec.Framework.graded
Graded and Bigraded Domains
Canonical Structures
Lemmas
Instances
Automation
Rec.Framework.sysf_types
System F Types
Types
Traversals & Evaluation
Renaming
Compatibility with renaming
Lifting traversals
Type Models
Naturality
Compatibility with instantiation
Miscellaneous Lemmas
Case Study: Instantiation on Types (Section 4)
Simple Traversals and Liftings (Section 8)
Rec.Framework.sysf_terms
Section 5: System F Terms and Values
Computations and Values
Traversals and their Evaluation
Models (Definition 5.4)
Renaming (Definition 5.6)
Lifting (Definition 5.5)
Theorem 5.8
Instantiation
Naturality
Compatibility with instantiation
Exports
Automation
Rec.Framework.sysf_const_terms
System F + constants Terms
Traversals and their Evaluation
Models (cf. Definition 5.4)
Renaming (cf. Definition 5.6)
Lifting (cf. Definition 5.5)
Theorem 5.8
Instantiation
Naturality
Compatibility with instantiation
Exports
Automation
Rec.Examples.sysf_typing
System F CBV Typing Relation
Typing traversal
Equations for recursive typing
Naturality
Relational Typing & Preservation
Rec.Examples.sysf_wn
Section 9 Case Study : Weak Normalisation of System FCBV
Big-step evaluation relation for FCBV
Simple traversal for weak normalisation (Definition 9.1)
Typing for FCBV
Semantic value and term typing
Fundamental theorem (Theorem 9.4)
Weak Normalisation
Rec.Examples.sysf_const_sn
Section 10 Case Study : Strong Normalisation of System F
One-Step Reduction
Many-Step Reduction
Syntactic typing
Strong Normalization
The Reducibility Candidates/Logical Predicate
Semantic typing (Definition 10.5)
The fundamental theorem
Strong normalisation
Rec.Extras.lambda_terms
Untyped Lambda Terms
Types
Traversals
Models
Renaming
Lifting
Instantiation
Naturality
Compatibility with instantiation
Simple models
Rec.Extras.lambda_model
Rec.Extras.sysf_print