An Interactive Proof of Termination for a Concurrent $\lambda$-calculus with References and Explicit Substitutions
Logic in Computer Science
2021-02-11 v1 Programming Languages
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.
Keywords
Cite
@article{arxiv.2102.05161,
title = {An Interactive Proof of Termination for a Concurrent $\lambda$-calculus with References and Explicit Substitutions},
author = {Yann Hamdaoui and Benoît Valiron},
journal= {arXiv preprint arXiv:2102.05161},
year = {2021}
}