An Interactive Proof of Termination for a Concurrent λ-calculus with References and Explicit Substitutions

2021/02/09 by Yann Hamdaoui, Hamdaoui, Yann, Benoît Valiron +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Programming Languages (cs.PL)

paper · pdf · doi:10.48550/arxiv.2102.05161

openalex publication_date 2021/02/09 · openalex created_date 2021/02/15 · openalex updated_date 2026/07/28

Abstract

In this paper we introduce a typed, concurrent λ-calculus with references featuring explicit substitutions for variables and references. Alongside usual safety properties, we recover strong normalization. The proof is based on a reducibility technique and an original interactive property reminiscent of the Game Semantics approach.

Related

• A decompilation of the pi-calculus and its application to termination
• Lambda Calculus with Explicit Read-back
• Termination of lambda-calculus with the extra Call-By-Value rule known as assoc
• Confluent terminating extensional lambda-calculi with surjective pairing and terminal type
• Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination