Joint work with Yannick Forster and Marc Roth
Advisor: Gert Smolka
Complexity theory uses Turing machines to define a time and space measure for algorithms. But it is difficulty and tediousness to reason about Turing machines and those definitions are rarely used in a rigorous way.
For two models of computation to agree to some extend in the notion of complexity, the Invariance thesis was formulated: "'Reasonable' machines can simulate each other within a polynomial bounded overhead in time and a constant-factor overhead in space."
We prove the Invariance Thesis between Turing machines and a call-by-value lambda calculus.
The proof of computational soundness of the two simulations is formalized in Coq. The complexity analysis is not yet formalized.