View: session overviewtalk overviewside by side with other conferences

09:00-10:00 Session 23E: Invited talk: Naoki Kobayashi
On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification
10:00-10:30 Session 25
Combinatorics of explicit substitutions (extended abstract)

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.

10:30-11:00Coffee Break
11:00-12:00 Session 26E: Invited talk: Pierre Vial
Some applications of quantitative types inside and outside type theory
12:00-12:30 Session 27
Orthogonality and sequentiality in substructural Linear HRSs

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.

12:30-14:00Lunch Break
14:00-15:00 Session 28E: Invited talk: Cynthia Kop
Wanda: a higher-order termination tool
15:00-15:30 Session 30B
Refining Properties of Filter Models: Sensibility, Approximability and Reducibility

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.

15:30-16:00Coffee Break
16:00-17:00 Session 31E
Normalization and Taylor expansion of lambda-terms

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 behaves well under the considered kind of reduction.

The next 700 (type-theoretical) denotational models ?

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.

19:45-22:00 Workshops dinner at Balliol College

Workshops dinner at Balliol College. Drinks reception from 7.45pm, to be seated by 8:15 (pre-booking via FLoC registration system required; guests welcome).

Location: Balliol College