We have the following invited speakers.
Often fairness assumptions need to be made in order to establish liveness properties of distributed systems, but in many situations they lead to false conclusions.
Here I present ongoing work aiming at laying the foundations of a theory of concurrency that is equipped to ensure liveness properties of distributed systems without making fairness assumptions. Instead I advocate assuming justness, a strong progress property that is essentially weaker and more realistic than fairness.
When assuming justness, contemporary process algebras and temporal logics fail to make distinctions between systems of which one has a crucial liveness property and the other does not. This necessitates an overhaul of these frameworks.
Type theories (in the sense of Martin-Löf and Coquand) are programming languages with type systems that are expressive enough to formulate mathematical statements. Several proof assistants, such as Agda, Lean, and Coq/Rocq, make use of this version of the Curry-Howard correspondence.
There are various interpretations of type theories, assigning different meanings to types. Traditionally, types were interpreted as propositions or sets, but since the advent of homotopy type theory, they are also seen as spaces. As a consequence, the correspondence between mathematical statements and types is not unique. For example, a group is usually represented as a carrier set with a unit element and an operation satisfying associativity, identity, and inverse laws. However, in homotopy type theory, it can alternatively be defined as a so-called "pointed connected 1-type".
In this talk, I will explain the ideas and insights that eventually led to homotopy type theory, along with an approach to computer formalizations that it enabled.
I will talk about an emerging new application of homotopy theory in computational complexity of discrete problems. This approach is build on the question: How does the topology of the solution space of a computational problem influence its complexity? The idea emerged from investigations of the complexity of variants of graph colouring, including approximate graph colouring.
A colouring of a graph with k colours is an assignment of colours to vertices under which no edge is monochromatic. Graph 3-colouring is a prototypical example of an NP-complete problem listed by Karp in his seminal paper. There are many variations on this problem whose complexity remains widely open. For example, although it is generally believed that colouring a 3-colourable graphs with a fixed number of colours is NP-hard, only hardness of colouring of such a graph with 5-colours is known (and shown only in 2019).
The talk will focus on several related results about variations of graph colouring that share a common theme of using a topological method based on tools from topological combinatorics and on ideas of Lovász [J. Comb. Theory, Ser. A, 25(3):319-324, 1978]. These ideas formalise the notion of a solution space, and hence provide a rigorous framework for the study of the above fundamental question.
Since the release of ChatGPT, large language models (LLMs) have been dominating the discourse around code generation. In contrast, the best-performing solvers in the world of formal program synthesis are still based around enumerative algorithms. So, are we behind the times? Are LLMs the answer to all our synthesis problems? In this talk, I will present two approaches to making the most of LLMs in formal domains. First, I will present a technique based on combining enumerative program synthesis with guidance from an LLM [1]. Focusing on the Syntax-Guided Synthesis (SyGuS) competition benchmarks, we found that, whilst LLMs can produce syntactically correct SyGuS expressions, they fail to produce semantically correct solutions for more than half of the benchmarks. We propose a novel enumerative synthesis algorithm, which integrates calls to an LLM into a weighted probabilistic search, allowing 2-way exchange of information between the two components, and increasing the number of benchmarks solved to 80% (and outperforming the state-of-the-art solver). Second, I will discuss our work using LLMs to generate models of systems for verification [2]. Here, we enable LLMs to generate syntactically correct code, even in programming languages that barely feature in the training data, by combining an HCI technique called natural program elicitation and a Max-SMT solver. We apply our approach to generating models of systems in the UCLID5 verification language, improving syntactic correctness from < 10% to > 80% on a set of textbook problems. Whilst I don’t believe LLMs are the answer to all our synthesis problems, I think our results demonstrate that perhaps techniques used in formal synthesis and programming languages could be the answer to many of the problems facing LLMs..!
[1] Guiding Enumerative Program Synthesis with Large Language Models. Yixuan Li, Julian Parsert, and Elizabeth Polgreen.
[2] Synthetic Programming Elicitation and Repair for Text-to-Code in Very Low-Resource Programming Languages. Federico Mora, Justin Wong, Haley Lepe, Sahil Bhatia, Karim Elmaaroufi, George Varghese, Joseph E. Gonzalez, Elizabeth Polgreen, and Sanjit A. Seshia.