## Contraction-aware lambda calculus

Institut für
Informatik

Ludwig-Maximilians-Universität
München

Monday 18 March 2002, 14:00

Cybernetica Bldg (Akadeemia tee 21), room B216

**Abstract**: A simply-typed lambda-calculus is presented whose
normal forms exactly represent the cut-free derivations of the
so-called contraction-free sequent calculus, invented independently by
Hudelmaier and Dyckhoff. Its crucial property is termination of proof
search without need for loop-detection.

The proposed lambda-calculus LambdaJT follows the paradigm of
generalized eliminations put forward by von Plato and consequently
also has permutative conversions. It will be shown that strong
normalization of the beta-reductions and permutative conversions
nevertheless can be established elegantly - even yielding an embedding
of the system with beta-reductions only into Girard's polymorphic
lambda-calculus. The full system, however, also has specific rules for
the elimination of contractions. Unfortunately, a proof of weak
normalization along the lines of the recent JSL paper by Dyckhoff and
Negri has not yet been successful: Although their lemmas could be
lifted to the more general situation of LambdaJT, the proof of
termination of the normalization algorithm is still missing.

**Slides from the talk**: 2up.ps.gz.

Tarmo Uustalu