Rencontre, 29 juin 2017

Programme

10:30 – 12:00

Marco Gaboardi (University at Buffalo, SUNY)

Invited talk: A semantic account of metric preservation in presence of probabilities.

Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical systems. A natural way to formalize program sensitivity is in terms of metric preservation with respect to the metrics on the input and output spaces: requiring that an r-sensitive function maps inputs that are at distance d to outputs that are at distance at most r*d. I will present some recent work where we started the study of program sensitivity and metric preservation from a denotational point of view. I will introduced metric CPOs, a novel semantic structure for reasoning about computation on metric spaces, by endowing CPOs with a compatible notion of distance. This structure is useful for reasoning about metric properties of programs, and specifically about program sensitivity and metric preservation. I will then discuss how to extend this structure to account for metrics over probability distributions. In particular, I will discuss how these metrics can be used to guarantee programs differentially private.

14:00 – 15:00

Marie Kerjean (IRIF)

Invited talk: Smooth models of Differential Linear Logic

While Linear Logic has been from the start strongly tied to algebra, it is only the later introduction of Differential Linear Logic (DiLL) that suggested similar ties with analysis. DiLL extends Linear Logic with differentiation, an operation which extracts a linear proof from a non-linear one. In this talk, I will present several models of DiLL interpreting formulas as topological vector spaces and proofs as smooth functions, thus strenghtening the analogy with (functional) analysis. I will explain a work with Y. Dabrowski highlighting how with a well chosen Mackey duality and under a specific completeness assumption, the multiplicative disjunction of LL corresponds to epsilon product of Schwartz. As opposed to the purely algebraic case, we can identify this connective with a well-known mathematical object. I will present a classical polarized model of a version of DiLL without promotion, where formulas are interpreted as nuclear spaces and where exponentials are interpreted as spaces of distributions. This models argues for a smooth Differential Linear Logic which, I will explain, hints for a type theory of differential equations.

15:30 – 16:30

Valentin Blot ( Queen Mary University of London)

Invited talk: An interpretation of system F through bar recursion

There are two possible computational interpretations of second-order arithmetic: Girard's system F or Spector's bar recursion and its variants. While the logic is the same, the programs obtained from these two interpretations have a fundamentally different computational behavior and their relationship is not well understood. We make a step towards a comparison by defining the first translation of system F into a simply-typed total language with a variant of bar recursion. This translation relies on a realizability interpretation of second-order arithmetic. Due to Gödel's incompleteness theorem there is no proof of termination of system F within second-order arithmetic. However, for each individual term of system F there is a proof in second-order arithmetic that it terminates, with its realizability interpretation providing a bound on the number of reduction steps to reach a normal form. Using this bound, we compute the normal form through primitive recursion. Moreover, since the normalization proof of system F proceeds by induction on typing derivations, the translation is compositional. The flexibility of our method opens the possibility of getting a more direct translation that will provide an alternative approach to the study of polymorphism, namely through bar recursion.