Project Page Index Table of Contents
  • Preliminaries
    • Abstract Reduction Systems
  • The call-by-value lambda calculus L
    • Syntax
    • Reduction
  • Correctness and time bounds
    • Correctness
    • Time bounds
  • Certifying extraction from Coq to L with time bounds
    • Extraction
      • Generation of Scott encodings
        • Examples
      • Generation of constructors
        • Examples
      • Extracting terms from Coq to L
        • Examples
      • Generation of encoding functions
    • Symbolic simplification for L
      • Lproc
      • Lbeta: symbolic beta reduction
      • Reflexted closure calculus
        • Closure calculus
      • Closure calculus interpreter
      • Lrewrite: simplification with corrextness statements
    • Tactics proving correctness
      • Interactive Demo
  • Encodings and extracted basic functions
    • Encoding of unit
    • Encoding of booleans
    • Encoding of natural numbers
    • Encoding of lists
    • Encoding of option type
    • Encoding of pairs
    • Encoding for L-terms
  • Extracted Functions
    • Extracted equality of encoded terms
    • Computability of Ackermann
  • Case Study 1: Universal L-term
    • Encoding for L-terms
    • Extracted equality on natural numbers
    • Extracted substitution
    • Extracted step-indexed L-interpreter
  • Case Study 2: Diophantine Equations
  • Case Study 3: Multi-Tape Turing Machines
    • Definition of TMs
    • Extraction of Turing Machine interpreter
      • Encoding finite types
      • Computability of functions with finite, discrete domain
      • Encoding vectors
      • Encoding tapes
      • Encoding configurations
      • Computability of transition relation
      • Computability of step-indexed interpreter
    • Turing machine halting reduces to L halting
Generated by coqdoc and improved with CoqdocJS