ABSTRACT. The relational semantics of linear logic is a powerful framework for defining resource-aware models of the λ-calculus. However, its quantitative aspects are not reflected in the preorders and equational theories induced by these models. Indeed, they can be characterized in terms of (in)equalities between Böhm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to define a quantitative contextual preorder on λ-terms, and demonstrate that it coincides with the preorder associated to the relational semantics, studied through non-idempotent intersection types.

ABSTRACT. Decidability of higher-order matching was established by Stirling via a sophisticated game-semantic argument. We propose an alternative specification of higher-order matching as an intersection type inhabitation problem. Concretely, we use the recently proposed system R, a syntax-directed intersection type system in which judgements derive vectors of types and binary relations control information flow between coordinates. Bounding the dimension of type vectors in system R derivations makes inhabitation in system R decidable. We outline how a solution to a higher-order matching instance corresponds to an inhabitant in system R of bounded dimension. The work is in progress; the central challenge is establishing a dimensional bound that depends only on the matching instance.

ABSTRACT. In this talk I will report on my efforts of using LLMs to (auto)formalize intersection type systems. Starting from a solid Agda codebase, I have been able to formalize soundness and completeness of several variants of non-idempotent intersection types, including the characterization of space consumption of a sophisticated abstract machine. I did this with almost no previous experience with proof assistants.

ABSTRACT. Relational semantics is a simple and well-studied denotational model for the untyped lambda-calculus. It can be presented syntactically as a non-idempotent intersection type system and provides qualitative and quantitative information, such as the characterization of normalizing terms and their execution time (i.e., the number of steps to reach the normal form). We study the relational semantics for the simply typed lambda-calculus extended with the fixpoint combinator; we show that the interpretation of a simply typed term is nothing but the interpretation of the untyped term restricted to the non-idempotent intersection types refining the simple type. Our approach is based on merging a simply typed derivation with a non-idempotent intersection one, which is not trivial since simply typed terms do not enjoy subject expansion and may not be normalizing (because of the fixpoint combinator). We also show that some well-known qualitative and quantitative completeness results provided by relational semantics and non-idempotent intersection type derivations for the untyped lambda-calculus lifts to the simply typed lambda-calculus with fixpoint combinator nearly for free, thanks to our results.