Project Page Index Table of Contents
  • Preliminaries
    • Natural Numbers
    • Lists
    • Relations
    • Misc
  • Call-by-value Lambda Calculus
    • Substitution
    • Reduction
    • Bound and Closedness for Terms
    • Stuck Terms
  • Machines and Refinements
  • Programms
  • Naive Stack Machine
  • Closures
    • Subtitution Lemmas
  • Closure Machine
  • Codes
  • Heaps
  • Heap Machine
  • Extras
    • Counterexample with open terms for closure machine
    • Properties of closedness
    • Weak computability of heap decompilation
    • Decompilation Function
Generated by coqdoc and improved with CoqdocJS