# Fabian Kunze: Research Immersion Lab

# The Invariance Thesis for a λ-Calculus:

## Towards Formal Complexity Theory

**Joint work** with Yannick Forster and Marc Roth

**Advisor:** Gert Smolka

## Abstract:

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

Legal notice, Privacy policy