Project Page Index Table of Contents
  • L: Weak Call-by-value Lambda Calculus
    • Substitution and Closedness
    • Deterministic Reduction
    • Resource Measures
      • Small-Step Time Measure
      • Small-Step Space Measure
      • Big-Step Time Measure
      • Big-Step Space Measure
  • Encoding Terms as Programs
    • Program size
    • Programm Decomposition
    • Program Substitution
    • Injectivity of Programm Encoding
  • Abstract Heap Machine
    • Heaps
    • Reduction Rules
    • Unfolding
    • Time
    • Space
    • Bonus: Unfolding on Programs
  • Abstract Substitution Machine
    • Reduction Rules
    • Time
    • Space
Generated by coqdoc and improved with CoqdocJS