Termination of Threads with Shared Memory via Infinitary Choice

Paolo Tranquilli (1)

1 LIP - Laboratoire de l'Informatique du Parallélisme

We present a static type discipline on an extension of lambda-calculus with threads and shared memory ensuring termination. This discipline is based on a type and effects system, and is a condition forced on regions. It generalizes and clarifies the stratification discipline previously proposed in the literature with the same objective, and is directly inspired by positive recursive types. The proof is carried out by translating the calculus with memory reference into an extension of lambda-calculus with a non-deterministic infinitary choice, whose strong normalization is in turn proved by a standard reducibility method.

Mots clés: lambda-calculus; termination; types and effects; concurrency

Domaines: Logique en informatique [cs.LO]

Paolo Tranquilli. Termination of Threads with Shared Memory via Infinitary Choice. 2011. ⟨hal-00573690⟩