Project Page Index Table of Contents
  • Axiomatic Assumptions
    • Functional Extensionality
    • Propositional Extensionality
  • Finite Types and Mappings
    • Forward Function Composition
    • Finite Types
      • Extension of Finite Mappings
      • Renamings and Injective Renamings
    • Notations
  • CBPV Types
    • Value Types
    • Computation Types
    • Ground Types
  • Semantics
    • Primitive Reduction
    • Operational Semantics
    • Context Semantics
    • Bigstep Semantics
    • Normal Form
    • Evaluation
    • Properties
  • Syntactic Typing Judement
    • Value Typing Judgement
    • Computation Typing Judgement
    • Type Preservation under Substitution
    • Preservation
    • Progress
  • Semantic Typing
    • Semantic Types
    • Semantic Soundness
      • Compatibility Lemmas
      • Semantic Soundness
  • Program Contexts
    • Value Contexts
    • Computation Contexts
    • Context Typing Judgement
    • Plugging Contexts into Contexts
      • Typing Soundness - Context Plugging
      • Plugging vs. Filling
    • Typing Soundness - Context Filling
  • Contextual Equivalence
  • Strong Reduction
    • Context Semantics
    • Recursive Semantics
      • Strong Step Equivalence Lemmas
      • Strong Step Progress
      • Weak to Strong
      • Strong Step Preservation
    • Compatibility with substitutions
    • Strong normalisation
    • Proper lemmas
    • Proper lemmas for plus
    • Inversion lemmas
  • Strong Semantic Typing
    • Saturation
    • Semantic Types
      • Properties of Semantic Types
    • Induction lemmas for closure
    • Semantic Soundness
      • Compatibility lemmas
      • Typing Lemmas
      • Semantic Soundness
  • Confluence
    • Parallel Reduction
    • Reduction Function
    • Properties
  • Eager let
    • Definition of eager let
    • Inversion for eager let
    • Typing for eager let
    • Eager let and substitutions
    • Eager let and reduction
    • Eager let is a congruence
      • Weak reduction
      • Strong reduction
  • Logical Equivalence
    • Logical Eqivalence
    • Properties of Logical Equivalence
      • Symmetry
      • Transitivity
      • Properties
    • Congruence Lemmas
      • Fundamental Property
      • Logical Equivalence is a congruence
    • Logical Equivalence Soundness
    • Reduction contained in equivalence
      • Reduction is contained in logical equivalence
      • Reduction is contained in observational equivalence
  • Denotational Semantics
    • Monads and Algebras
      • Monad
      • T-Algebra
      • Free T-Algebra
      • Singleton T-Algebra
      • Product T-Algebra
      • Exponential T-Algebra
    • Denotational Semantics
      • Denotation of Value Types
      • Denotation of Computation Types
      • Denotation of Typing Contexts
      • Denotation of Values
      • Denotation of Computations
      • Preservation of denotational equality in contexts
    • Logical Relation
      • Value Relations
      • Computation Relations
    • Adequacy
      • Grountypes Contextual Equivalence
      • Basic Lemma
      • Adequacy
      • Soundness
  • Simply typed, Fine-Grained CBV
    • Typing
    • Translation CBV - CBPV
      • Translation and Substiution Commute
      • Translation injective
  • Weak Reduction CBN
    • Forward Simulation
    • Termination
    • Backward Simulation
    • Simulation
  • Strong Reduction CBV
    • Forward Simulation
    • Backward Simulation
  • Denotational Semantics CBV
    • Contexts
    • Alternative translation
    • Observational Equivalence by translation
    • Denotational Semantics
  • Simply typed CBN
    • Typing
    • Typing under renaming and substitution
    • Translation relation from CBN to CBPV
      • Translation and substitution commute
    • Translation functions from CBN to CBPV
      • Translation is well-behaved
      • Translation of substitutions
      • Translation of substitutions is well-behaved for renamings
    • Extended translation relation
      • Translation injective
  • Weak Reduction CBN
    • Forward Simulation
    • Backward Simulation
    • Translation and substitution commute
  • Strong reduction CBN
    • Forward simulation
    • Backward Simulation
  • Denotational Semantics CBN
    • Contexts
    • Alternative translation
    • Observational Equivalence by translation
    • Denotational Semantics
  • Normalisation
    • Weak Normalisation
    • Strong Normalisation
    • Termination by Soundness of Denotational Semantics
  • Equational Theory
    • Strong Equivalence
    • Levy Equations
      • eta laws
      • sequencing laws
      • additional equations
Generated by coqdoc and improved with CoqdocJS