ABSTRACT. Barendregt’s book “The Lambda Calculus, its syntax and semantics”(1981/84) has become a ‘classic’ in Theoretical Computer Science because it presents the state of the art in lambda calculus at that time in a comprehensive way. Moreover, a number of open problems and conjectures were proposed. In 2022, Barendregt and Manzonetto published a ‘sequel’ of this book, presenting the solutions of several of these problems, and more. In this talk, I will present a selection of these problems and the key ingredients that were employed in their solutions

ABSTRACT. When substitutions and bindings interact, there is a risk of undesired side-effects if the substitution is applied naïvely. The λ-calculus captures this phenomenon in an abstract setting, as β-reduction may require the renaming of bound variables to avoid variable capture. In this paper we introduce α-paths as a characterisation for α-avoidance. These paths provide a novel method to predict and analyse the need for α in different λ-calculi. In particular, we show how α-paths charaterise α-avoidance for seemingly unrelated calculi like (i) developments, (ii) affine λ-calculus, (iii) weak λ-calculus, (iv) safe λ-calculus. Further, we study the unavoidablity of α-conversions in untyped and simply-typed calculi and prove undecidability of the need of α-conversions in the former context for leftmost–outermost reductions. The presented method has been implemented in a tool.

ABSTRACT. This paper defines two decreasing measures for terms of the simply typed lambda-calculus, called the Z-measure and the A-measure. A decreasing measure is a function that maps each typable lambda-term to an element of a well-founded ordering, in such a way that contracting any beta-redex decreases the value of the function, entailing strong normalization. Both measures are defined constructively, relying on an auxiliary calculus, a non-erasing variant of the lambda-calculus. In this system, dubbed the lambdaG-calculus, each beta-step creates a "bin" containing a copy of the argument that cannot be erased and cannot interact with the context in any other way. Both measures rely crucially on the observation, known to Turing and Prawitz, that contracting a redex cannot create redexes of higher degree, where the degree of a redex is defined as the height of the type of its lambda-abstraction. The Z-measure maps each lambda-term to a natural number, and it is obtained by evaluating the term in the lambdaG-calculus and counting the number of remaining bins. The A-measure maps each lambda-term to a structure of nested multisets, where the nesting depth is proportional to the maximum redex degree.

ABSTRACT. This work introduces a quantitative version of the simple type assignment system, starting from a suitable restriction of non-idempotent intersection types. The key idea is to restrict multiset formation to uniform types, two types being uniform if they differ only in the cardinality of the multisets occurring in it. The resulting system, which we call system U, has the same typability power as the simple type assignment system; thus, assigning types to terms supplies the very same qualitative information given by simple types, but at the same time provides some interesting quantitative information. It is well known that typability for simple types is equivalent to unification; we prove a similar result for the newly introduced system U, and propose a typing algorithm. More precisely, we show that typability is equivalent to a unification problem which is a non-trivial extension of the classical one: in addition to unification rules, our typing algorithm makes use of an operation, called expansion, which increases the cardinality of multisets whenever needed.

ABSTRACT. We are concerned with understanding the nature of program metrics for calculi with higher-order types, seen as natural generalisations of program equivalences. Some of the metrics we are interested at are well-known, such as one based on the interpretation of terms in metric spaces and one obtained by generalising observational equivalence. We also introduce a new one, called the interactive metric, built by applying the well-known Int-Construction to the category of metric complete partial orders. Our aim is then to understand how these metrics relate to each other, i.e., whether and in which cases one such metric is a refinement of another, in analogy with the corresponding well-studied problem about program equivalences. The results we get are twofold. We first show that the metrics of semantic origin, i.e., the denotational and interactive ones, lie between the observational and equational metrics and that in some cases, such inclusions are strict. Then, we give a result about the relationship between the denotational and interactive metrics, which tells us that the former is at most as discriminating as the latter. All our results are given for a linear lambda-calculus, and some of them can be generalised to calculi with graded comonads, in the style of Fuzz.

ABSTRACT. We present a generalization of Spector's bar recursion to the Diller-Nahm variant of Gödel's Dialectica interpretation. This generalized bar recursion collects witnesses of universal formulas in sets of approximation sequences to provide an interpretation to the double-negation shift principle. The interpretation is presented in a fully computational way, implementing sets via lists. We also present a demand-driven version of this extended bar recursion manipulating partial sequences rather than initial segments. We explain why in a Diller-Nahm context there seems to be several versions of this demand-driven bar recursion, but no canonical one.

ABSTRACT. We investigate the cyclic proof theory of extensions of Peano Arithmetic by (finitely iterated) inductive definitions. Such theories are essential to proof theoretic analyses of certain `impredicative' theories; moreover, our cyclic systems naturally subsume Simpson's Cyclic Arithmetic.

Our main result is that cyclic and inductive systems for arithmetical inductive definitions are equally powerful. We conduct a metamathematical argument, formalising the soundness of cyclic proofs within second-order arithmetic and appealing to conservativity. This approach is inspired by those of Simpson and Das for Cyclic Arithmetic, however we must further address a difficulty that the closure ordinals of our inductive definitions (around Church-Kleene) far exceed the proof theoretic ordinal of the appropriate metatheory (around Bachmann-Howard or Bucholz), and so explicit induction on their notations is not possible. For this reason, we rather rely on a formalisation of the theory of (recursive) ordinals within second-order arithmetic.

ABSTRACT. Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles in various settings. In its most general form, the guardedness discipline applies to general symmetric monoidal categories and further specializes to Cartesian and co-Cartesian categories, where it governs guarded recursion and guarded iteration respectively. Here, even more specifically, we deal with the semantics of call-by-value guarded iteration. It was shown by Levy, Power and Thielecke that call-by-value languages can be generally interpreted in Freyd categories, but in order to represent effectful function spaces, such a category must canonically arise from a strong monad. We generalize this fact by showing that representations of guarded effectful function spaces must rely on certain parametrized monads (in the sense of Uustalu). This provides a description of guardedness as an intrinsic categorical property of programs, complementing the existing description of guardedness as a predicate.