ABSTRACT. lambda-upsilon is an extension of the lambda-calculus which internalises the calculus of substitutions. In the current paper, we investigate the combinatorial properties of lambda-upsilon focusing on the quantitative aspects of substitution resolution. We exhibit an unexpected correspondence between the counting sequence for lambda-upsilon terms and famous Catalan numbers. As a by-product, we establish effective sampling schemes for random lambda-upsilon terms. We show that typical lambda-upsilon terms represent, in a strong sense, non-strict computations in the classic lambda-calculus. Moreover, typically almost all substitutions are in fact suspended, i.e., unevaluated, under closures. Consequently, we argue that lambda-upsilon is an intrinsically non-strict calculus of explicit substitutions. Finally, we investigate the distribution of various redexes governing the substitution resolution in lambda-upsilon and investigate the quantitative contribution of various substitution primitives.

ABSTRACT. The aim of this work is to characterize three fundamental normalization proprieties in lambda-calculus trough the Taylor expansion. The general proof strategy consists in stating the dependence of ordinary reduction strategies on their resource counterparts and in finding a convenient resource term in the support of the Taylor expansion that well-behaves under the considered kind of reduction.

ABSTRACT. Linear HRSs are higher-order rewriting systems having the substructural linear lambda-calculus as a substitution calculus. We explore the properties of orthogonality and sequentiality, focusing on multiplicative and additive conjunction, and how they differ in behaviour to `intuitionistic' HRSs.

ABSTRACT. In this paper, we study the tedious link between the properties of sensibility and approximability of models of untyped λ-calculus. Approximability is known to be a slightly, but strictly stronger property that sensibility. However, we will see that so far, each and every (filter) model that have been proven sensible are in fact approximable. We explain this result as a weakness of the sole known approach of sensibility: the Tait reducibility candidates and its realizability variants.

In fact, we will reduce the approximability of a filter model D for the λ-calculus to the sensibility of D but for an extension of the λ-calculus that we call λ-calculus with D-tests. Then we show that traditional proofs of sensibility of D for the λ-calculus are smoothly extendable for this λ-calculus with D-tests.

ABSTRACT. The use of intersection type systems in the the study of denotational semantics of the untyped λ-calculus has been a fruitful line of research over the past thirty-five years. In this extended abstract we present a research project aiming at broaden the boundaries of such type-theoretical approach to semantics, possibly to other idealized programming languages. The key idea is to ex- ploit a more abstract view on what a type system is. This view finds its root in higher-dimensional category theory.