Abstract The two Girard translations provide two different means of obtaining embeddings of Intuitionistic Logic into Linear Logic, corresponding to different lambda-calculus calling mechanisms. The translations, mapping $$A\rightarrow B$$ A → B respectively to $${!}{A}\multimap B$$ ! A ⊸ B and $${!}{(A\multimap B)}$$ ! ( A ⊸ B ) , have been shown to correspond respectively to call-by-name and call-by-value. In this work, we split the of-course modality of linear logic into two modalities, written “ $${!} $$ ! ” and “ $$\bullet $$ ∙ ”. Intuitively, the modality “ $${!} $$ ! ” specifies a subproof that can be duplicated and erased, but may not necessarily be “accessed”, i.e. interacted with, while the combined modality “ $${!}{\bullet }$$ ! ∙ ” specifies a subproof that can moreover be accessed. The resulting system, called $$\textsf{MSCLL}$$ MSCLL , enjoys cut-elimination and is conservative over $$\textsf{MELL}$$ MELL . We study how restricting access to subproofs provides ways to control sharing in evaluation strategies. For this, we introduce a term-assignment for an intuitionistic fragment of $$\textsf{MSCLL}$$ MSCLL , called the $$\lambda ^{{!}{\bullet }}$$ λ ! ∙ -calculus, which we show to enjoy subject reduction, confluence, and strong normalization of the simply typed fragment. We propose three sound and complete translations that respectively simulate call-by-name, call-by-value, and a variant of call-by-name that shares the evaluation of its arguments (similarly as in call-by-need). The translations are extended to simulate the Bang-calculus, as well as weak reduction strategies.

When translating a term calculus into a graphical formalism many inessential details are abstracted away. In the case of $\lambda$-calculus translated to proof-nets, these inessential details are captured by a notion of equivalence on $\lambda$-terms known as $\simeq_\sigma$-equivalence, in both the intuitionistic (due to Regnier) and classical (due to Laurent) cases. The purpose of this paper is to uncover a strong bisimulation behind $\simeq_\sigma$-equivalence, as formulated by Laurent for Parigot's $\lambda\mu$-calculus. This is achieved by introducing a relation $\simeq$, defined over a revised presentation of $\lambda\mu$-calculus we dub $\Lambda M$. More precisely, we first identify the reasons behind Laurent's $\simeq_\sigma$-equivalence on $\lambda\mu$-terms failing to be a strong bisimulation. Inspired by Laurent's \emph{Polarized Proof-Nets}, this leads us to distinguish multiplicative and exponential reduction steps on terms. Second, we enrich the syntax of $\lambda\mu$ to allow us to track the exponential operations. These technical ingredients pave the way towards a strong bisimulation for the classical case. We introduce a calculus $\Lambda M$ and a relation $\simeq$ that we show to be a strong bisimulation with respect to reduction in $\Lambda M$, ie. two $\simeq$-equivalent terms have the exact same reduction semantics, a result which fails for Regnier's $\simeq_\sigma$-equivalence in $\lambda$-calculus as well as for Laurent's $\simeq_\sigma$-equivalence in $\lambda\mu$. Although $\simeq$ is formulated over an enriched syntax and hence is not strictly included in Laurent's $\simeq_\sigma$, we show how it can be seen as a restriction of it.

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting systems. We study the problem of extending the notion of proof term to higher-order rewriting, which generalizes the first-order setting by allowing terms with binders and higher-order substitution. In previous works that devise proof terms for higher-order rewriting, such as Bruggink’s, it has been noted that the challenge lies in reconciling composition of proof terms and higher-order substitution (β-equivalence). This led Bruggink to reject "nested" composition, other than at the outermost level. In this paper, we propose a notion of higher-order proof term we dub rewrites that supports nested composition. We then define two notions of equivalence on rewrites, namely permutation equivalence and projection equivalence, and show that they coincide.

The purpose of this paper is to identify programs with control operators whose reduction semantics are in exact correspondence. This is achieved by introducing a relation $\simeq$, defined over a revised presentation of Parigot's $λμ$-calculus we dub $ΛM$. Our result builds on two fundamental ingredients: (1) factorization of $λμ$-reduction into multiplicative and exponential steps by means of explicit term operators of $ΛM$, and (2) translation of $ΛM$-terms into Laurent's polarized proof-nets (PPN) such that cut-elimination in PPN simulates our calculus. Our proposed relation $\simeq$ is shown to characterize structural equivalence in PPN. Most notably, $\simeq$ is shown to be a strong bisimulation with respect to reduction in $ΛM$, i.e. two $\simeq$-equivalent terms have the exact same reduction semantics, a result which fails for Regnier's $σ$-equivalence in $λ$-calculus as well as for Laurent's $σ$-equivalence in $λμ$.

Justification Logic is a refinement of modal logic where the modality is annotated with a reason s for “knowing” A and written . The expression s is a proof of A that may be encoded as a lambda calculus term of type A, according to the propositions-as-types interpretation. Our starting point is the observation that terms of type are reductions between lambda calculus terms. Reductions are usually encoded as rewrites essential tools in analyzing the reduction behavior of lambda calculus and term rewriting systems, such as when studying standardization, needed strategies, Lévy permutation equivalence, etc. We explore a new propositions-as-types interpretation for Justification Logic, based on the principle that terms of type are proof terms encoding reductions (with source s). Note that this provides a logical language to reason about rewrites.

Resource types are types that statically quantify some aspect of program execution. They come in various guises; this paper focusses on a manifestation of resource types known as non-idempotent intersection types. We use them to characterize weak normalisation for a type-erased lambda calculus for the Calculus of Inductive Construction (λe), as introduced by Gregoire and Leroy. The λe calculus consists of the lambda calculus together with constructors, pattern matching and a fixed-point operator. The characterization is then used to prove the completeness of a strong call-by-need strategy for λe. This strategy operates on open terms: rather than having evaluation stop when it reaches an abstraction, as in weak call-by-need, it computes strong normal forms by admitting reduction inside the body of abstractions and substitutions. Moreover, argument evaluation is by-need: arguments are evaluated when needed and at most once. Such a notion of reduction is of interest in areas such as partial evaluation and proof-checkers such as Coq.

Justification Logic ( JL ) is a refinement of modal logic in which assertions of knowledge and belief are accompanied by justifications: the formula 〚s〛A states that s is a ‘reason’ for knowing/believing A . We study the computational interpretation of JL via the Curry–Howard isomorphism in which the modality 〚s〛A is interpreted as: s is a type derivation justifying the validity of A . The resulting lambda calculus is such that its terms are aware of the reduction sequence that gave rise to them. This serves as a basis for understanding systems, many of which belong to the security domain, in which computation is history-aware.

The Propositional Logic of Proofs (LP) is a modal logic in which the modality □A is revisited as [​[t]​]​A , t being an expression that bears witness to the validity of A . It enjoys arithmetical soundness and completeness, can realize all S4 theorems and is capable of reflecting its own proofs ( ⊢A implies ⊢[​[t]​]A , for some t ). A presentation of first-order LP has recently been proposed, FOLP, which enjoys arithmetical soundness and has an exact provability semantics. A key notion in this presentation is how free variables are dealt with in a formula of the form [​[t]​]​A(i) . We revisit this notion in the setting of a Natural Deduction presentation and propose a Curry–Howard correspondence for FOLP. A term assignment is provided and a proof of strong normalization is given.

We present a call-by-need strategy for computing strong normal forms of open terms (reduction is admitted inside the body of abstractions and substitutions, and the terms may contain free variables), which guarantees that arguments are only evaluated when needed and at most once. The strategy is shown to be complete with respect toβ-reduction to strong normal form. The proof of completeness relies on two key tools: (1) the definition of a strong call-by-need calculus where reduction may be performed inside any context, and (2) the use of non-idempotent intersection types. More precisely, terms admitting aβ-normal form in pure lambda calculus are typable, typability implies (weak) normalisation in the strong call-by-need calculus, and weak normalisation in the strong call-by-need calculus implies normalisation in the strong call-by-need strategy. Our (strong) call-by-need strategy is also shown to be conservative over the standard (weak) call-by-need.

Standardization is a fundamental notion for connecting programming languages and rewriting calculi. Since both programming languages and calculi rely on substitution for defining their dynamics, explicit substitutions (ES) help further close the gap between theory and practice.

The Pure Pattern Calculus (PPC) extends the lambda-calculus, as well as the family of algebraic pattern calculi, with first-class patterns; that is, patterns can be passed as arguments, evaluated and returned as results. The notion of matching failure of the PPC not only provides a mechanism to define functions by pattern matching on cases but also supplies PPC with parallel-or-like, non-sequential behaviour. Therefore, devising normalising strategies for PPC to obtain well-behaved implementations turns out to be challenging. This paper focuses on normalising reduction strategies for PPC. We define a (multistep) strategy and show that it is normalising. The strategy generalises the leftmost-outermost strategy for lambda-calculus and is strictly finer than parallel-outermost. The normalisation proof is based on the notion of necessary set of redexes, a generalisation of the notion of needed redex encompassing non-sequential reduction systems.

We defineBACI(Boxed Ambients with Communication Interfaces), an ambient calculus with a flexible communication policy. Traditionally, typed ambient calculi have a fixed communication policy determining the kind of information that can be exchanged with a parent ambient, even though mobility changes the parent.BACIlifts that restriction, allowing different communication policies with different parents during computation. Furthermore,BACIseparates communication and mobility by making the channels of communication between ambients explicit. In contrast with other typed ambient calculi where communication policies are global, each ambient inBACIis equipped with a description of the communication policies ruling its information exchange with parent and child ambients. The communication policies of ambients increase when they move: more precisely, when an ambient enters another ambient, the entering ambient and the host ambient can exchange their communication ports and agree on the kind of information to be exchanged. This information is recorded locally in both ambients. We show the type-soundness ofBACI, proving that it satisfies the subject reduction property, and we study its behavioural semantics by means of a labelled transition system.

High-level specification of patterns of communications such as protocols can be modeled elegantly by means of session types (Honda et al ., 1998). However, a number of examples suggest that session types fall short when finer precision on protocol specification is required. In order to increase the expressiveness of session types we appeal to the theory of correspondence assertions (Clarke & Marrero, 1998; Gordon & Jeffrey, 2003b). The resulting type discipline augments the types of long-term channels with effects and thus yields types which may depend on messages read or written earlier within the same session. This new type system can be used to check: source of information, whether data is propagated as specified across multiple parties, if there are unspecified communications between parties, and if the data being exchanged has been modified by the code in an unspecified way. We prove that evaluation preserves typability and that well-typed processes are safe. Also, we illustrate how the resulting theory allows us to address shortcomings present in the pure theory of session types.

In this paper we encode higher-order rewriting with names into higher-order rewriting in de Bruijn notation. This notation not only is defined for terms (as usually done in the literature) but also for metaterms, which are the syntactical objects used to express the rewriting rules of higher-order systems. Several examples are discussed. Fundamental properties such as confluence and normalisation are shown to be preserved.

We define a formal encoding from higher-order rewriting into first-order rewriting modulo an equational theory ℰ. In particular, we obtain a characterization of the class of higher-order rewriting systems which can be encoded by first-order rewriting modulo an empty equational theory (that is, ℰ = ∅). This class includes of course the λ-calculus. Our technique does not rely on the use of a particular substitution calculus but on an axiomatic framework of explicit substitutions capturing the notion of substitution in an abstract way. The axiomatic framework specifies the properties to be verified by a substitution calculus used in the translation. Thus, our encoding can be viewed as a parametric translation from higher-order rewriting into first-order rewriting, in which the substitution calculus is the parameter of the translation.