ABSTRACT. Graph rewriting systems can be used to specify computation and more generally to specify and analyse the dynamics of complex systems. They provide visual, intuitive models that are directly executable. In this talk, we will describe the use of strategic port graph rewriting as a visual modelling tool and its implementation in PORGY. In the first part of the talk we will present hierarchical higher-order port graphs (HOPs, an extension of port graphs with graph variables and nesting), and a notion of HOP rewriting following the SPO (Single PushOut) approach. In the second part of the talk, we will describe PORGY (a port-graph rewriting tool) and give examples of application of HoP rewriting: the specification of a lambda-calculus evaluator and a simple model of rational negligence in financial markets.

ABSTRACT. Please find both the 2-page abstract and the 2-page CV in the attached document.

ABSTRACT. Partial differential equations (PDEs) are ubiquitous tools used in modeling problems such as the motion of fluids, the flow of current in electric circuits, the dissipation of heat in solid objects, the propagation and detection of seismic waves, or the increase or decrease of populations, etc. Among the most well-known examples of PDEs are the Maxwell equation for electric and magnetic fields, the Navier-Stokes equation for fluid mechanics, the Schrödinger equation for quantum mechanics, the Laplace equation, the wave equation and the heat equation. Analytical solutions of partial differential equations are always useful in engineering analysis because they provide a better understanding of the physical importance of different parameters affecting the problem. In this project, we propose to use higher-order logic theorem proving to analyze PDEs. The main motivation is highly expressive and sound nature of higher-order logic which can be used to effectively model any system that can be expressed in a closed mathematical form.

ABSTRACT. Despite its critical role, remote attestation in Intel Software Guard Extensions (SGX) and Trust Domain Extensions (TDX) is not only underspecified by Intel but also contains various contradictions that could potentially lead to design and implementation flaws. We take the challenge of formal specification and verification of remote attestation mechanism in Intel SGX and TDX.

ABSTRACT. Hybrid systems are used to model cyber-physical systems such as autonomous vehicles or medical devices. Due to their safety-critical nature and their high cost, it is important to be able to prevent errors at the design stage. One way to do it is to use an interactive theorem prover where the system is formally defined and the relevant properties are stated as logical formulas. The KeYmaera X prover and some work done in Isabelle/HOL are good examples where this approach has been successfully applied to real-world systems.

Two key properties that we are interested in checking are safety and stability. Proving safety involves showing that some set of unsafe states cannot be reached. There are various definitions of stability but the main idea is to ensure that the trajectories of the dynamical system converge and are robust to perturbations of the initial conditions. While theorem provers provide a convenient framework for high-level reasoning of these properties, the proofs require complicated numerical computations that are more suitable to be performed by a specialised numerical solver. It turns out that both safety and stability can often be reduced to convex optimisation problems, where a solver is used to find a barrier certificate or a Lyapunov function respectively. The reduction is not trivial and many side conditions need to be checked. Moreover, in some cases, it would be highly desirable to also verify the certificate, which involves reasoning about floating-point errors or recovering an exact solution.

Integrating symbolic provers with numerical solvers is a long-standing challenge in the formal methods community. Lean 4 has been designed to be easily extended and has many other features such as a rich macro system and efficient code generation that make it a good candidate to build this interface. For these reasons, it is the research vehicle of choice for this project. Its mathematical library has been growing at a fast pace and, in particular, in the analysis section, there are most of the key definitions and lemmas needed to reason about convex optimisation.

My initial exploration of Lean's metaprogramming capabilities led to the development of a sum-of-squares tactic to solve real inequalities. Sum-of-squares is a particular application of semidefinite optimisation very relevant to verifying polynomial systems. For rational polynomials, finding an exact decomposition might require very large denominators even for relatively simple cases. However, there are a few tricks to mitigate this issue and some tools such as RealCertify can solve a large number of examples. One of my goals is to incorporate some of these ideas into the Lean tactic. Another approach is the one taken by ValidSPD, written in Coq, where they reason about round-off errors to deduce non-negativity. I have developed a simple model of floating-point arithmetic in Lean and made progress towards the development of a similar tactic.

Beyond semidefinite and sum-of-squares programming, we would like to take advantage of Lean to verify any convex optimisation problem. One of the main objectives of this project has been to develop various parts of CvxLean, which aims to be a verified version of CvxPy. This is joint work with Dr Alexander Bentkamp and Prof Jeremy Avigad. In this framework, a convex optimisation problem can be defined in a familiar syntax and a tactic reduces it to conic form following the rules of disciplined convex programming. There are also capabilities to define custom functions and reductions. My main contribution has been the 'solve' command, which encodes the reduced problem and sends it to MOSEK, a popular convex optimisation tool. Then it constructs a Lean term from the solution, which the user can access. We have been able to formalise some relevant examples with applications in statistics such as covariance estimation, which shows that it is feasible to perform these transformations in a verified way whilst preserving efficiency and illustrates the usefulness of having an ambience mathematical library. For example, the spectral theorem for symmetric matrices and the theory of Schur complements were needed to prove some of the side conditions.

Moving forward, the library will be extended with more functions and custom tactics for different types of optimisation goals. By default, the solver is trusted and only in some very basic examples, a full proof can be constructed so some more work is needed to handle larger instances. Regarding applications, my focus will be to encode queries about the safety and stability of hybrid systems.

ABSTRACT. I discuss my research, which is focused on formalising nominal AC-unification. Completed and remaining research are presented along with publication plans.

ABSTRACT. Realms are a proposed high-level structuring concept for theory graphs that abstracts over isomorphic formalizations of the same concept. But it is a relatively complex language feature, and it is difficult to assess if its practical value outweighs the cost of implementing it. We investigate to what extent realms can be achieved as a design pattern (as opposed to a primitive feature) in existing formal systems. Concretely, we present multiple formalizations in the MMT system and identify what minimal additional language features would yield realm-like benefits. Our evaluation is that this approach is promising, and we propose a small set of generally useful features that allow realm-like formalizations.

ABSTRACT. Sophize is a novel mathematics library and discussion platform with a mission to help our users find and organize mathematical proofs. We present Sophize's novel yet familiar knowledge organization scheme that is used to represent a wide variety of proofs. With this scheme at its core, we have engineered a platform to logically aggregate knowledge from multiple sources. The platform curates knowledge from published research, encyclopaedias such as PlanetMath and Wikipedia, informal computer programs, and formal systems such as Metamath; and allows its users to run a federated search over them. To make this happen, two developments were necessary. First, we came up with the concept of 'proof-generating machines' and developed an open plugin architecture that allows proofs from computer programs to be generated as required. Second, we extended the Markdown language to represent the connections between mathematical objects found across various sources of knowledge. In addition, we also utilized this new language to create a novel communication system built specifically to aid mathematicians in solving problems collaboratively.

ABSTRACT. The Galois group of an infinite Galois extension has a natural topology, called the Krull topology, which has the important property of being profinite. It is impossible to talk about Galois representations, and hence the Langlands Program, without first defining the Krull topology. We explain our formalisation of this topology, and our proof that it is profinite, in the Lean 3 theorem prover. The paper emphasises technical aspects of our implementation and discusses some of the computational issues we faced.

ABSTRACT. This paper describes a dataset of lemma templates extracted from Isabelle’s Archive of Formal Proofs. A template is an expression describing the shape of a given lemma. We hypothesise that many lemmas and theorems have similar shapes, and that knowledge of common shapes and their frequencies and correlations can be useful for downstream tasks such as automated conjecturing.

ABSTRACT. PISE is an application for representing, studying, and annotating informal proofs from the mathematical literature. PISE aims to provide the equivalent for mathematics of an annotated chess game at chess.com, or the detailed and clickable driving directions available in Google maps. In systems of this kind, there is a graphical display, and a textual discussion. Clicking links in the text side navigates and advances the graphics. PISE does all this with informal mathematical proofs, by representing them in a semi-formal argument mapping system. Its purpose is to make mathematical literature more accessible. This can aid both in contemporary communication, as well is in the genetic method of studying and learning mathematics through its historic literature.