Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userAn Interactive Proof of Termination for a Concurrent $lambda$-calculus with References and Explicit Substitutions
107
0
0.0
(
0
)
Added by
Yann Hamdaoui
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
In this paper we introduce a typed, concurrent $lambda$-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.
rate research
Read More
In this paper, we show how to interpret a language featuring concurrency, references and replication into proof nets, which correspond to a fragment of differential linear logic. We prove a simulation and adequacy theorem. A key element in our translation are routing areas, a family of nets used to implement communication primitives which we define and study in detail.
Cartesian difference categories are a recent generalisation of Cartesian differential categories which introduce a notion of infinitesimal arrows satisfying an analogue of the Kock-Lawvere axiom, with the axioms of a Cartesian differential category being satisfied only up to an infinitesimal perturbation. In this work, we construct a simply-typed calculus in the spirit of the differential lambda-calculus equipped with syntactic infinitesimals and show how its models correspond to difference lambda-categories, a family of Cartesian difference categories equipped with suitably well-behaved exponentials.
We present the guarded lambda-calculus, an extension of the simply typed lambda-calculus with guarded recursive and coinductive types. The use of guarded recursive types ensures the productivity of well-typed programs. Guarded recursive types may be transformed into coinductive types by a type-former inspired by modal logic and Atkey-McBride clock quantification, allowing the typing of acausal functions. We give a call-by-name operational semantics for the calculus, and define adequate denotational semantics in the topos of trees. The adequacy proof entails that the evaluation of a program always terminates. We introduce a program logic with Lob induction for reasoning about the contextual equivalence of programs. We demonstrate the expressiveness of the calculus by showing the definability of solutions to Ruttens behavioural differential equations.
A genoid is a category of two objects such that one is the product of itself with the other. A genoid may be viewed as an abstract substitution algebra. It is a remarkable fact that such a simple concept can be applied to present a unified algebraic approach to lambda calculus and first order logic.
We present a type system to guarantee termination of pi-calculus processes that exploits input/output capabilities and subtyping, as originally introduced by Pierce and Sangiorgi, in order to analyse the usage of channels. We show that our system improves over previously existing proposals by accepting more processes as terminating. This increased expressiveness allows us to capture sensible programming idioms. We demonstrate how our system can be extended to handle the encoding of the simply typed lambda-calculus, and discuss questions related to type inference.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
