This work provides the first inductive definition of useful CBV evaluation. For that, we first restrict the substitution operation in the Value Substitution Calculus to be linear, yielding the LCBV strategy. We then further restrict substitution in LCBV, so that substitution contributes to the progress of the computation. This optimisation is the UCBV strategy, and its notion of substitution is sensitive to the surrounding evaluation context, so it is non-trivial to capture it inductively. Moreover, we show that UCBV is a sound and complete implementation of LCBV, optimised to implement useful evaluation. As a further contribution, we show that an existing notion of usefulness in the literature, namely the GLAMoUr abstract machine, implements the UCBV strategy with polynomial overhead in time. This establishes that UCBV is time-invariant, i.e., that the number of reduction steps to normal form in UCBV can be used as a measure of time complexity. Defining UCBV leads us to the first semantic model of useful CBV evaluation through system U, a non-idempotent intersection type system. Our main result is a characterisation of termination for useful CBV evaluation via system U: a term is typable in system U if and only if it terminates in UCBV. Additionally, system U provides a quantitative interpretation for UCBV, offering exact step-count information for program evaluation. Even though the specification of the operational semantics of UCBV is highly complex, system U is notably simple. As far as we know, system U is one of the scarce quantitative type systems capturing exactly the substitution step-count for a call-by-value strategy.

Abstract Useful evaluation is an optimised evaluation mechanism for functional programming languages, introduced by Accattoli and Dal Lago. The key to useful evaluation is to represent programs with sharing and to implement substitution of terms only when this contributes to the progress of the computation. Initially defined in the framework of call-by-name, useful evaluation has since been extended to call-by-value. The definitions of usefulness in the literature are complex and lack inductive structure, which makes it challenging to (formally) reason about them. In this work, we define useful call-by-value evaluation inductively, proceeding in two stages. First, we refine the well-known Value Substitution Calculus , so the substitution operation becomes linear , yielding the $$\textsc {lcbv} $$ L C B V calculus. The two calculi are observationally equivalent. We then further refine $$\textsc {lcbv} $$ L C B V by restricting linear substitution only when it contributes to the progress of the computation, yielding the $$\textsc {ucbv} $$ U C B V strategy. This new substitution notion is sensitive to the surrounding evaluation context, so it is non-trivial to capture it inductively. Moreover, we formally show that the resulting $$\textsc {ucbv} $$ U C B V is a sound and complete implementation of $$\textsc {lcbv} $$ L C B V , optimised to implement useful evaluation. As a further contribution, we show that the $$\textsc {ucbv} $$ U C B V strategy can be implemented by an existing lower-level abstract machine called GLAMoUr with polynomial overhead in time. This entails, as a corollary, that $$\textsc {ucbv} $$ U C B V is time-invariant , i.e. , that the number of reduction steps to normal form in $$\textsc {ucbv} $$ U C B V can be used as a measure of time complexity. Our $$\textsc {ucbv} $$ U C B V strategy is part of the preliminary work required to develop semantic interpretations of useful evaluation, for which its inductive formulation is more suitable than the (non-inductive) existing ones.

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.

Intersection type systems have been independently applied to different evaluation strate- gies, such as call-by-name (CBN) and call-by-value (CBV). These type systems have been then generalized to different subsuming paradigms being able, in particular, to encode CBN and CBV in a unique unifying framework. However, there are no intersection type systems that explicitly enable CBN and CBV to cohabit together, without making use of an encoding into a common target framework. This work proposes an intersection type system for a specific notion of evaluation for PCF, called PCFH. Evaluation in PCFH actually has a hybrid nature, in the sense that CBN and CBV operational behaviors cohabit together. Indeed, PCFH combines a CBV- like behavior for function application with a CBN-like behavior for recursion. This hybrid nature is reflected in the type system, which turns out to be sound and complete with respect to PCFH: not only typability implies normalization, but also the converse holds. Moreover, the type system is quantitative, in the sense that the size of typing derivations provides upper bounds for the length of the reduction sequences to normal form. This first type system is then refined to a tight one, offering exact information regarding the length of normalization sequences. This is the first time that a sound and complete quantitative type system has been designed for a hybrid computational model.

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 lambda-PRK-calculus is a typed lambda-calculus that exploits the duality between the notions of proof and refutation to provide a computational interpretation for classical propositional logic. In this work, we extend lambda-PRK to encompass classical second-order logic, by incorporating parametric polymorphism and existential types. The system is shown to enjoy good computational properties, such as type preservation, confluence, and strong normalization, which is established by means of a reducibility argument. We identify a syntactic restriction on proofs that characterizes exactly the intuitionistic fragment of second-order lambda-PRK, and we study canonicity results.

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.

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.

It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ES that is halfway between small-step calculi and traditional calculi with ES. This paper studies the relationship between the LSC and environment-based abstract machines. While traditional calculi with ES simulate abstract machines, the LSC rather distills them: some transitions are simulated while others vanish, as they map to a notion of structural congruence. The distillation process unveils that abstract machines in fact implement weak linear head reduction, a notion of evaluation having a central role in the theory of linear logic. We show that such a pattern applies uniformly in call-by-name, call-by-value, and call-by-need, catching many machines in the literature. We start by distilling the KAM, the CEK, and a sketch of the ZINC, and then provide simplified versions of the SECD, the lazy KAM, and Sestoft's machine. Along the way we also introduce some new machines with global environments. Moreover, we show that distillation preserves the time complexity of the executions, i.e. the LSC is a complexity-preserving abstraction of abstract machines.