Youyou Cong (Tokyo Institute of Technology)
Composing Music from Types
The Curry-Howard isomorphism tells us that a well-typed program satisfies the specification represented by its type. By extending this idea, we can guarantee that well-typed music adheres to the composition rules represented by its type. In this talk, I will present an ongoing study on composing correct music using types. I will share the results so far, describe the identified challenges, and discuss possible applications.
Ekaterina Komendantskaya (Heriot-Watt University)
Refine and Synthesise: a type-theoretic view on neural network robustness.
Safety and security are critical for some complex AI systems involving neural networks, yet they are difficult to ensure. The most famous instance of this problem is guaranteeing robustness against adversarial attacks. Intuitively, a neural network is ε-ball robust for an image if, when you move no more than ε away from it in the input space, the output does not change much, or alternatively, the classification decision that the network gives does not change. Adversarial robustness is a property that even very accurate neural networks fail to satisfy.
Seeing that a neural network is a function N : [ℝ] → ℝ (we use [ℝ] to represent a vector), the above verification problem can actually be cast as a type refinement problem. We define an ε-ball B(x,ε) around a sample input x of that class: B(x,ε) = {x’ ∈ [ℝ] : ‖ x’ − x ‖ ≤ ε}, and then prove that any object in B(x, ε) will be classified as y. It now amounts to imposing a refinement type on N : (x : [ℝ] {‖ x’ − x ‖ 2 ≤ ε}) → (y : ℝ{y = y}), for some given image x’.
Traditionally, languages with refinement types rely on SMT solvers for type checking, and type checking robust definitions of neural networks will require specialised solvers, such as Marabou, for efficiency. Moreover, as very few neural networks are robust, we often need to retrain N and obtain its robust version N’ in order to successfully type check N’ : (x : [ℝ] {‖ x’ − x ‖ 2 ≤ ε}) → (y : ℝ{y = y}). And this procedure strongly resembles type-driven program synthesis!
In this talk, I will explain the intricacies of this approach by discussing several different mathematical definitions of robustness that arise in literature on adversarial training and neural network verification. I will pay special attention to showing how these different definitions affect “type checking” and “program synthesis” for neural networks.
Sam Lindley (University of Edinburgh)
On the expressive power of types
Just over three decades ago Felleisen published an influential paper on the expressive power of programming languages. He observed that the existing literature covered a variety of informal notions of expressiveness. He then proposed macro expressiveness, a formal characterisation of local transformations, as a means for capturing the intuitions underlying many of those notions.
One aspect of programming languages that Felleisen did not consider was types. Types provide additional structure that can be used both to complement macro expressiveness and to specify alternative, sometimes richer, notions of expressiveness. In this talk I will present several examples exploring the expressiveness of typed programming languages. I will focus on examples that I find interesting, surprising, or amusing. An underlying message I will seek to convey is the fragility of expressivity results and hence the importance of carefully describing the context before claiming that a particular language, feature, or type is more expressive than another.
Leonardo de Moura (Microsoft Research)
The Lean 4 theorem prover and programming language
Lean 4 is an implementation of the Lean interactive theorem prover (ITP) in Lean itself. It addresses many shortcomings of the previous versions and contains many new features. Lean 4 is fully extensible: users can modify and extend the parser, elaborator, tactics, decision procedures, pretty printer, and code generator. The new system has a hygienic macro system custom-built for ITPs. It contains a new typeclass resolution procedure based on tabled resolution, addressing significant performance problems reported by the growing user base. Lean 4 is also an efficient functional programming language based on a novel programming paradigm called functional but in-place. Efficient code generation is crucial for Lean users because many write custom-proof automation procedures in Lean itself.
