• Marie Kerjean (CNRS, Université Sorbonne Paris Nord)

Title: From functional analysis to proofs and programs

Abstract: In this talk, we will survey some of the motivations and challenges for interpreting proofs as functions in continuous settings, and the computational features that one can extract from traditional functional analysis. 

Through the well-known Curry-Howard correspondence, programs are typed by proofs which can in turn be interpreted as functions between spaces. Taking this road in the reverse sense allows to extract from functions new paradigms in logic. The historic examples for that is linearity, which went from an algebraic to a computational notion. Triggered in part by the applications of probabilistic and differential programming, there is a motivation to make notions from analysis take the same road. We will explain how one can make differentiation and distribution theory fit in the setting of proof theory. We will show of this generalizes the notion of resource used by a program to the one of solution to a differential equation. Finally, we will show of functional analysis gives us a monadic setting for the quantitative interpretation of proof and programs.

• Sandra Alves (University of Porto)

Title: Quantitative Weak Linearisation

Abstract: Weak linearisation was defined years ago through a static characterisation of the intuitive notion of virtual redex, based on (legal) paths computed from the (syntactical) term tree. Weak-linear terms impose a linearity condition only on functions that are applied (consumed by reduction) and functions that are not applied (therefore persist in the term along any reduction) can be non-linear. This class of terms was shown to be strongly normalising with deciding typability in polynomial time. We revisit this notion through non-idempotent intersection types (also called quantitative types). By using an effective characterisation of minimal typings, based on the notion of tightness, we are able to distinguish between “consumed” and “persistent” term constructors, which allows us to define an expansion relation, between general lambda-terms and weak-linear lambda-terms, whilst preserving normal forms by reduction.