Related papers: A journey through resource control lambda calculi …
In this paper we investigate the $\lambda$ -calculus, a $\lambda$-calculus enriched with resource control. Explicit control of resources is enabled by the presence of erasure and duplication operators, which correspond to thinning and…
We introduce the \emph{resource control cube}, a system consisting of eight intuitionistic lambda calculi with either implicit or explicit control of resources and with either natural deduction or sequent calculus. The four calculi of the…
This paper concerns the explicit treatment of substitutions in the lambda calculus. One of its contributions is the simplification and rationalization of the suspension calculus that embodies such a treatment. The earlier version of this…
We present a typing system with non-idempotent intersection types, typing a term syntax covering three different calculi: the pure {\lambda}-calculus, the calculus with explicit substitutions {\lambda}S, and the calculus with explicit…
We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard…
Many different systems with explicit substitutions have been proposed to implement a large class of higher-order languages. Motivations and challenges that guided the development of such calculi in functional frameworks are surveyed in the…
We extend intersection types to a computational $\lambda$-calculus with algebraic operations \`a la Plotkin and Power. We achieve this by considering monadic intersections, whereby computational effects appear not only in the operational…
Programs with control are usually modeled using lambda calculus extended with control operators. Instead of modifying lambda calculus, we consider a different model of computation. We introduce continuation calculus, or CC, a deterministic…
In the first part of this paper, we define two resource aware typing systems for the {\lambda}{\mu}-calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial…
In this paper, we present an explicit substitution calculus which distinguishes between ordinary bound variables and meta-variables. Its typing discipline is derived from contextual modal type theory. We first present a dependently typed…
Randomized higher-order computation can be seen as being captured by a lambda calculus endowed with a single algebraic operation, namely a construct for binary probabilistic choice. What matters about such computations is the probability of…
Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that…
We present some lambda calculus with explicit substitutions and named variables. The characteristic feature of this calculus is as follows: renaming of bound variables when performing substitutions is done using special reductions and may…
The resource calculus is an extension of the lambda-calculus allowing to model resource consumption. It is intrinsically non-deterministic and has two general notions of reduction - one parallel, preserving all the possible results as a…
Calculi with control operators have been studied to reason about control in programming languages and to interpret the computational content of classical proofs. To make these calculi into a real programming language, one should also…
We characterize those intersection-type theories which yield complete intersection-type assignment systems for lambda-calculi, with respect to the three canonical set-theoretical semantics for intersection-types: the inference semantics,…
We investigate program equivalence for linear higher-order(sequential) languages endowed with primitives for computational effects. More specifically, we study operationally-based notions of program equivalence for a linear…
The lambda calculus since more than half a century is a model and foundation of functional programming languages. However, lambda expressions can be evaluated with different reduction strategies and thus, there is no fixed cost model nor…
We study an assignment system of intersection types for a lambda-calculus with records and a record-merge operator, where types are preserved both under subject reduction and expansion. The calculus is expressive enough to naturally…
We present two rewriting systems that define labelled explicit substitution lambda-calculi. Our work is motivated by the close correspondence between Levy's labelled lambda-calculus and paths in proof-nets, which played an important role in…