Rencontre, 6 février 2025

Programme

• Justin Hsu (Cornell University)
  Invited talk: Type Systems for Numerical Error Analysis

  Programs in numerical analysis and scientific computing make heavy use of floating-point numbers to approximate ideal real numbers. Operations on floating-point numbers incur roundoff error, and an important practical problem is to bound the overall magnitude of the error for complex computations. Existing work employs a variety of strategies such as interval arithmetic, SMT encodings, and global optimization; however, current methods are not compositional and are limited in scalability, precision, and expressivity.

  Today, I'll talk about some of our recent work on NumFuzz, a higher-order language that can bound forward error using a linear, coeffect type system for sensitivity analysis combined with a novel quantitative error type. Our type inference procedure can derive precise relative error bounds for programs that are several orders of magnitude larger than previously possible.

  If time permits, I'll briefly discuss a second type system called Bean for bounding backward error. Like NumFuzz, Bean is based on a linear coeffect type system, but it features a semantics based on a novel category of lenses on metric spaces. Bean is the first system to soundly reason about backward error in numerical programs.

  Joint work with Ariel Kellison (Cornell).

  • 6 février 2025, 10:30
• Shin-Ya Katsumata (Kyoto Sangyo University)
  Invited talk: Codensity liftings and their applications to semantics

  Codensity lifting is a method to construct liftings of endofunctors/monads along fibrations. They subsume several constructions in mathematics, such as the Kantorovich metric and the lower/upper preorders on powersets. In this talk, I will give an overview of codensity lifting and its applications to program semantics and formalization of bisimulations over coalgebras.

• Valentin Maestracci (Université Aix-Marseille)
  Invited talk: The Lambda Calculus can be Quantified

  In this paper we introduce several quantitative methods for the lambda-calculus based on partial metrics, a well-studied variant of standard metric spaces that have been used to metrize non-Hausdorff topologies, like those arising from Scott domains. First, we study quantitative variants, based on program distances, of sensible equational theories for the λ-calculus, like those arising from Böhm trees and from the contextual preorder. Then, we introduce applicative distances capturing higher-order Scott topologies, including reflexive objects like the D∞ model. Finally, we provide a quantitative insight on the well-known connection between the Böhm tree of a λ-term and its Taylor expansion, by showing that the latter can be presented as an isometric transformation.