View: session overviewtalk overviewside by side with other conferences
09:00 | On Two Kinds of Higher-Order Model Checking and Higher-Order Program Verification |
10:00 | SPEAKER: Maciej Bendkowski 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. |
11:00 | Some applications of quantitative types inside and outside type theory |
16:00 | 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. |
16:30 | The next 700 (type-theoretical) denotational models ? SPEAKER: Domenico Ruoppolo 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. |
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).