相关论文: Strong Normalizability as a Finiteness Structure v…

In our paper "Uniformity and the Taylor expansion of ordinary lambda-terms" (with Laurent Regnier), we studied a translation of lambda-terms as infinite linear combinations of resource lambda-terms, from a calculus similar to Boudol's…

The aim of this work is to characterize three fundamental normalization proprieties in lambda-calculus trough the Taylor expansion of $ \lambda$-terms. The general proof strategy consists in stating the dependence of ordinary reduction…

It has been known since Ehrhard and Regnier's seminal work on the Taylor expansion of $\lambda$-terms that this operation commutes with normalization: the expansion of a $\lambda$-term is always normalizable and its normal form is the…

Originating in Girard's Linear logic, Ehrhard and Regnier's Taylor expansion of $\lambda$-terms has been broadly used as a tool to approximate the terms of several variants of the $\lambda$-calculus. Many results arise from a Commutation…

We show that the normal form of the Taylor expansion of a $\lambda$-term is isomorphic to its B\"ohm tree, improving Ehrhard and Regnier's original proof along three independent directions. First, we simplify the final step of the proof by…

We generalise Ehrhard and Regnier's Taylor expansion from pure to probabilistic $\lambda$-terms through notions of probabilistic resource terms and explicit Taylor expansion. We prove that the Taylor expansion is adequate when seen as a way…

We introduce a calculus of extensional resource terms. These are resource terms \`a la Ehrhard-Regnier, but in infinitely eta-long form. The calculus still retains a finite syntax and dynamics: in particular, we prove strong confluence and…

We extend the recently introduced setting of coherent differentiation for taking into account not only differentiation, but also Taylor expansion in categories which are not necessarily (left)additive. The main idea consists in extending…

We introduce the structural resource lambda-calculus, a new formalism in which strongly normalizing terms of the lambda-calculus can naturally be represented, and at the same time any type derivation can be internally rewritten to its…

We consider the untyped lambda calculus with constructors and recursively defined constants. We construct a domain-theoretic model such that any term not denoting bottom is strongly normalising provided all its `stratified approximations'…

We give a type system in which the universe of types is closed by reflection into it of the logical relation defined externally by induction on the structure of types. This contribution is placed in the context of the search for a natural,…

Twenty years after its introduction by Ehrhard and Regnier, differentiation in $\lambda$-calculus and in linear logic is now a celebrated tool. In particular, it allows to establish a Taylor expansion formula for various $\lambda$-calculi,…

The differential $\lambda$-calculus studies how the quantitative aspects of programs correspond to differentiation and to Taylor expansion inside models of linear logic. Recent work has generalized the axioms of Taylor expansion so they…

Many applications of denotational semantics, such as higher-order model checking or the complexity of normalization, rely on finite semantics for monomorphic type systems. We exhibit such a finite semantics for a polymorphic purely linear…

We study the semantics of a resource-sensitive extension of the lambda calculus in a canonical reflexive object of a category of sets and relations, a relational version of Scott's original model of the pure lambda calculus. This calculus…

In this paper, we present a general realizability semantics for the simply typed $\lambda\mu$-calculus. Then, based on this semantics, we derive both weak and strong normalization results for two versions of the $\lambda\mu$-calculus…

A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed $\lambda$-terms, defined using denotational…

The call-by-value lambda calculus can be endowed with permutation rules, arising from linear logic proof-nets, having the advantage of unblocking some redexes that otherwise get stuck during the reduction. We show that such an extension…

We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity…

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…