Fabian Kunze: Research Immersion Lab

Saarland University Computer Science

The Invariance Thesis for a λ-Calculus:

Towards Formal Complexity Theory

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.

Documents and Proof Scripts

Fabian Kunze, Fri Jan 13 16:09:19 2017