CIRCA

News

CIRCA seminar February 22nd


There will be a CIRCA lunchtime seminar on 22nd Feb at 1pm in Theatre D of Maths.

Chris Brown and Victoria Ironmonger will speak.

Chris’s Title: Semi-Automatic Ladderisation: Improving Code Security through Rewriting and Dependent Types
Chris’s Abstract: Cyber attacks become more and more prevalent every day. An arms race is thus engaged between cyber attacks and cyber defences. One type of cyber attack is known as a side channel attack, where attackers exploit information leakage from the physical execution of a program, e.g. timing or power leakage, to uncover secret information, such as encryption keys or other sensitive data. There have been various attempts at addressing the problem of side-channel attacks, often relying on various measures to decrease the discernibility of several code variants or code paths. Most techniques require a high-degree of expertise by the developer, who often employs ad hoc, hand-crafted code-patching in an attempt to make it more secure. In this talk, we take a different approach: building on the idea of ladderisation, inspired by Montgomery Ladders. We present a semi-automatic tool-supported technique, aimed at the non-specialised developer, which rewrites (a class of) C programs into functionally (and even algorithmically) equivalent counterparts with improved security properties. Our rewriting mechanism provides refactorings that transform the source code into its ladderised equivalent, driven by an underlying verified rewrite system, based on dependent types. Our rewrite system automatically finds rewritings of C programs producing their equivalent ladderised counterparts for a subset of C. We demonstrate our ladder rewriting technique on a number of representative examples from the cryptographic domain, showing increased security thanks to the process.

Victoria’s Title: The atomicity problem for equivalence relations and other structures
Victoria’s Abstract: An atomic poset is one which cannot be expressed as a union of two proper subsets. Atomic sets are sometimes called ideals, and atomicity is equivalent to the joint embedding property. We look at posets where two combinatorial structures are related when one is a substructure of the other. Given such a poset, avoidance sets are subsets defined by their forbidden substructures. The atomicity problem asks whether it is decidable, given a finite set, whether its avoidance set is atomic. We will discuss the atomicity problem for various structures, finishing by solving it for equivalence relations under the non-consecutive order. In this, we show that an avoidance set is atomic if and only if each forbidden element has only one class size.

CIRCA seminar February 8th


There will be a CIRCA lunchtime seminar on 8th Feb at 1pm in Theatre D of Maths.

Coen del Valle and Ruth Hoffmann will speak.

Coen’s title: It’s not always bad to be greedy
Coen’s abstract: A base for a group of permutations of a set \Omega is a subset of \Omega whose pointwise stabiliser contains only the identity permutation. In this talk we discuss a natural greedy algorithm for building a base. In 1999, Cameron conjectured that there is some absolute constant, c, such that for any primitive group, G, every greedy base for G has size at most c times that of a minimum base for G. We discuss new results towards a proof of this conjecture, namely that it holds whenever G is either symmetric or alternating, except for a class of possible exceptions. Time permitted we may also describe an interesting application in graph theory.

Ruth’s title: Composable Constraint Models for Permutation Pattern Enumeration Problems
Ruth’s abstract: I will give an introduction to permutation patterns, discuss a few pattern types as well as porperties and show on an example how constraint programming has helped breaking the current state of the art (specialised) methods to enumerate permutation pattern problems.
In particular we will look at the 1324 avoiding permutations for which to date there still is no defined growth function. We progressed the enumeration for 1324 avoiding permutations with some additional properties/constraints (namely permutations with a fixed number of inversions) and identified a unique sequence in the OEIS to this problem. This was made possible through the creation of a library of constraint models for many of the permutation pattern types, properties and statistics. This library was created with composability in mind, so that we can offer mathematicians a neat ‘copy and paste’ library from which they can create their own bespoke model for the permutation pattern problems with a selection of properties.

CIRCA seminar January 25th


The first CIRCA seminar of the year is on January 25th in Theatre D of Maths at 1pm.

Speaker: Carla Biermann
Title: Sampling solutions to constraint satisfaction problems
Abstract: State-of-the-art constraint programming solvers have become efficient in finding one solution to a specified problem. However, sometimes, users would like to choose a solution from multiple or inspect a sample of solutions without obtaining all solutions, especially when the solution space is large. This need gives rise to solution sampling, which aims to provide the user with an interesting sample of solutions. There are different measures of “interestingness” and algorithms that ensure certain sampling behaviours. I will present two such algorithms and the results of an experimental analysis of their performance on specific constraint satisfactory problems (CSPs). The findings aim to spark a discussion with the audience on more applications of solution sampling in CSPs for my fourth-year project.

and

Speaker: Nguyen Dang
Title: Automated algorithm configuration and algorithm selection
Abstract: Many algorithms have their own parameters that can impact the algorithm performance. Automated algorithm configuration is a family of general-purpose techniques that focuses on finding the best parameter setting of an algorithm for a given problem. Automated algorithm selection, on the other hand, is a closely related topic that helps us select the best algorithm among a given set of algorithms for a specific instance of a problem. Automated algorithm configuration and algorithm selection have got several successful applications across different domains. In this talk, I will first give a brief introduction to the two topics. The remaining part of the talk will be an open discussion with the audience to see if there are potential applications of those techniques on the GAP system.

CIRCA seminar 30th November


There will be a CIRCA seminar on November 30th, at 1pm on Theatre D of Maths. Peter Cameron and Richard Connor will speak.

Peter’s title is “When is the commuting graph split or threshold?”.

Abstract: The commuting graph of a group (or semigroup) G has vertex set G, two vertices joined if they commute. It was introduced by Brauer and Fowler in 1955, in their seminal work on involution centralisers in simple groups.
Split graphs and threshold graphs are two subgraph-closed graph families arising in operations research. A graph is split if the vertex set is the union of a complete graph and a null graph (with maybe some edges between); it is threshold if there are vertex weights and two vertices are joined if the sum of their weights exceeds a threshold.
I hope to present the complete proof of the classification of groups whose commuting graph is split or threshold: they are either abelian, or generalised dihedral of twice odd order.

Richard’s title is “Similarity search by graph navigation: some high-dimensional problems”

Abstract: Similarity search is a simple concept: to (efficiently) find, from within a (very) large collection, those objects which are most similar to a query object presented from the same domain. We (kind of) know that even approximate search becomes linear-time when the data is “high dimensional”, and linear time is no use to us! Unfortunately, “high” means something like over 20 Euclidean dimensions, and our main current interest is in searching embeddings, which are high-dimensional vectors arising from convolutional neural networks (such as GPT.) Language model embeddings have thousands of dimensions.

Some interesting recent systems have emerged which use novel graph navigation techniques. Simply, each element of the collection is represented as a graph node, and nodes are connected according to some relation. Search strategy is something like: start at a random node and navigate the graph, at each step moving closer to the query, which should thus be reached in a logarithmic number of steps. The current “state-of-the-art” is hnswlib (Hierarchical Navigable Small-World), which claims to work independently of dimensionality.

That, of course, isn’t true! In this talk, we examine the essential concepts presented by the authors, and some unfortunate properties of high-dimensional spaces which spoil the low-dimensional intuitions of graph navigation.

All welcome!

CIRCA seminar 16th November


There will be a CIRCA seminar on 16th November, at 1pm in Theatre D of Maths.

Mun See Chang will speak on “Enriching Transformations for Dependently Typed Languages”.

Ursula Martin will speak on “The Social Machine of Mathematics”

Ursula’s abstract is: How does mathematics come about? In this talk I’ll look at what philosophers, social scientists and historians can tell us about what we are doing when we do mathematics, including recent work on explanation in mathematics, and on how mathematics has impact. I’ll also highlight new approaches to collaborative mathematics, computer supported formal proof, and AI-assisted proof, which challenge our understanding of what a proof might be.

All welcome!

CIRCA seminar 2nd November


There will be a CIRCA seminar on November 2nd, at 1pm in Theatre D of Maths.

Edwin Brady will speak on “The Idris Programming Language”

Details: I will talk about the Idris Programming Language, a language which (like Lean) is based on dependent type theory and (unlike Lean :)) is developed primarily in St Andrews with help from researchers and developers around the world. It is intended for general purpose programming, and supports formal reasoning about those programs. I will give some introductory examples which show how programming and theorem proving interact, and show how we are using dependent type theory to help develop robust and verifiable software.

Jon Fraser will speak on “Fourier analysis in finite fields”.

Details: I will discuss various counting problems in vector spaces over finite fields and show how a ‘Fourier analytic’ approach can help.

All welcome!

CIRCA seminar 5th October


On 5th October at 1pm in Maths D, Peiran Wu will talk about Lean, the theorem prover. We’ll then discuss setting up a study group to put some group theory into Lean. All welcome.

First CIRCA seminar of the year


There will be a CIRCA seminar on Thursday 21st September at 1pm in Theatre D of Maths.

Ian Miguel will speak on Puzznic and Colva Roney-Dougal will count the subgroups of the symmetric group.

Visit of Arne Van Antwerpen


Arne Van Antwerpen will be here on 16/17/18 May, visiting Olexandr Konovalov.

Arne will give a CIRCA seminar on the Wednesday afternoon, 4-5 in Theatre C.

Title: Multipermutation solutions of the Yang-Baxter equation and nilpotency of skew braces

Abstract: This talk will be based on joint work with Eric Jespers and Leandro Vendramin. The class of multipermutation solutions is a particularly interesting class of solutions of the celebrated Yang-Baxter equation (coming from mathematical physics) with a beautiful combinatorial structure. It was shown that this class corresponds to right nilpotent skew left braces of nilpotent type. In this talk we delve deeper into this class of skew left braces and identify the class of centrally nilpotent skew braces. We discuss that these behave very similar to nilpotent groups and will identify several possible central series for these objects. If time permits, we use this class to illustrate several other key concepts of skew left braces. The talk will be rife with examples and exciting open problems.

All welcome!

Visit of Pascal Schweitzer


Pascal Schweitzer from TU-Darmstadt will visit CIRCA on Wednesday May 10th, and give a talk at 4pm in Maths C. All welcome.