- Preliminaries
- Shared libraries
- Finitary sums and products over monoids
- Binomial theorem
- Bitwise operations on nat as list bool
- Bitwise operations on nat
- Euclidian division and Bezout's identity
- Prime numbers
- Base p representation
- Reification for bounded quantification
- Pidgeon hole principle
- Iteration of binary relations
- Traditional Definition
- Inductive Definition
- Binary PCP
- Binary Post correspondence problem with indices
- Decidability and Enumerability
- Many-One Reductions
- Post's Theorem and Markov's Principle
- Post Correspondence Problem
- First-Order Logic
- Tarski Semantics
- Natural Deduction
- Kripke Semantics
- FOL Reductions
- Intuitionistic FOL
- Classical Natural Deduction
- Weakening
- Infinite Data Types
- Definitions
- SRH to SR
- SR to MPCP
- MPCP to PCP
- PCP to CFP
- PCP to CFI
- TM to SRH
- Post grammars are context-free
- CFP to CFI
- Code
- A certified low-level compiler
- Binary Stack Machines
- Minsky Machines
- Intuionistic Linear Logic
- List of all results
- Formal Undecidability
- Alternate Minsky Machines such that two counters are enough for undec
- Minsky machines to FRACTRAN programs
- Arithmetic libraries for Matiyasevich's theorems
- Object-level representation of Diophantine equations
- Diophantine logic
- Elementary diophantine constraints
- Single Diophantine equations
- Object-level encoding of exponential
- Object-level encoding of bounded universal quantification I
- Object-level encoding of bounded universal quantification II
- Object-level encoding of bounded universal quantification III
- Reflexive transitive closure is Diophantine
- FRACTRAN termination is Diophantine
- Main undecidability results and DPRM theorem
- Basis for the full TM library
- Relations
- Definition of Multi-Tape Turing Machines
- 0-tape Turing machine that does nothing.
- Basic 1-Tape Machines
- Primitive Two-tape machines
- Combinators
- Switch Combinator
- Mirror Operator
- Tapes-Lift
- Tactic Support
- Alphabet-Lift
- Tactics that help verifying complex machines
- Simple compound multi-tape Machines
- Move to a symbol and translate read symbols
- Copy Symbols from t0 to t1
- Compare two tapes (from left to right) until a symbol is reached
- Codable Class
- Value-Containing
- Alphabet-lift for "programmed" Turing Machines
- Copying Machines and Helper functions for verifying machines using CopySymbols ane MoveToSymbol
- Compare two values
- All tools for programming Turing machines
- Constructor and Deconstructor Machines for Natural Numbers
- Constructor and Deconstructor Machines for Sum Types and Option Types
- Constructor and Deconstructor Machines for Lists
- Constructors and Deconstructors for Finite Types
- Constructors and Deconstructors for Pair Types
- Machines that compte natural functions
- Machines that compute list functions
- Encoding for binary numbers
- Pointer bookkeeping for machines using (positive) binary numbers
- Machine for comparing two positive binary numbers
- Machines for shifting positive binary numbers
- Multiplication of positive numbers
- Machines on N (binary natural numbers)
- Lookup an entry in an associative list
- Universal Turing Machine
- Definitions and Automation for PrettyBounds
- Automation
- Maximum element in a list
- PrettyBounds for Machines in TM/Code
- PrettyBound for Univ
- Bounds For M2M
- Case Study: Place usage for list machines
- Space Analysis for Univ
- Theorem: Univ can simulate multi-tape Turing machines with polynominal time and linear space overhead
- Preliminaries
- The call-by-value lambda calculus L
- Correctness and time bounds
- Certifying extraction from Coq to L with time bounds
- Encodings and extracted basic functions
- Extracted Functions
- Extracted equality of encoded natural numbers
- Extracted equality of encoded terms
- Extracted encoding of natural numbers
- Extracted term encoding
- Decidabiity of closedness, boundedness and procness
- Extracted size of terms
- Extracted substitution on terms
- Extracted step-indexed L-interpreter
- Computability of full evaluation
- Enumeratibility of L-terms
- Computability of Ackermann
- Extraction of Turing Machine interpreter
- Reducing halting problem for TMs to halting problem for L
- Diophantine Equations
- Resource Measures
- Abstract L machines
- Computability in L
- Definition of L-acceptability
- Properties of acceptance
- L-acceptable predicates are closed under conjunction and disjunction
- L-ecidable predicates are L-acceptable (and their complement too)
- Definition of L-decidability
- Complement, conj and disj of predicates
- Deciders for complement, conj and disj of ldec predicates
- L-decidable predicates are closed under complement, conj and disj
- First Fixed Point Theorem
- Second Fixed Point Theorem
- Definition of parallel or
- The self halting problem is not L-acceptable
- Rice's Theorem
- Applications of Rice's Theorem
- Rice's Theorem, classical, on combinators
- Scott's Theorem
- Applications of Scott's Theorem
- Step indexed evaluation
- Properties of star:
- Semantics of the Heap Machine
- Alphabets
- Constructors and Deconstructors for Comens
- Heap Lookup
- Implementation of ϕ (aka SplitBody)
- Step Machine of the Heap Machine Simulator
- Reduction of the Halting Problem of the Heap Machine to the Halting Problem of Turing Machines
- PrettyBounds for LM
- Axiomatic Assumptions
- Syntax
- Semantics
- Equational Theory
- Simple Typing
- Order Typing
- Terms Extension
- Confluence
- Weak Normalisation
- Evaluator
- Higher-Order Unification
- System Unification
- Nth-Order Unification
- Enumerability
- PCP and MPCP
- Third-Order Encoding
- Simplified Reduction
- Huet Reduction
- Higher-Order Motivation
- Second-Order Realisation
- Conservativity
- Constants
- Enumerability from Conservativity
- First-Order Unification
- L to TM