Project Page
Index
Table of Contents
Preliminaries
Lists
Tactics
Post Corresepondence Problem
Post correspondence problem over natural numbers
Binary Post correspondence problem
Binary Post correspondence problem with indices
PCP reduces to BPCP
BPCP reduces to iBPCP
Code
Syntax
Semantics
Compisitional Reasoning over Subcode
A certified low-level compiler
Semantic Correctness of Compiled Code
A Syntactically Correct Compiler
Binary Stack Machines
Semantics for BSM
iBPCP reduces to BSM
BSM recues to MM
Minsky Machines
Semantics for MM
Simulating Binary Stacks with numbers
Intuionistic Linear Logic
eILL reduces to ILL
MM reduces to eILL
List of all results
Formal Undecidability