Currently undertaken as an MSc research project by Alex Alferovs but similar projects will be available in the future.
A central concept in theoretical cryptography are so-called one-way functions. They are defined in terms of complexity, probability and asymptotics — which, on the face of it, implies that any proofs about them will also need to venture into those three areas. This project aims to improve on that by gathering and enhancing a collection of algebraic properties of one-way functions and their combinations. This will allow for proofs and constructions that use one-way functions as black boxes.
Program refinement normally goes from "more abstract" to "more concrete" programs, with the difference being measured formally or informally, e.g. in the amount of non-determinism or the amount of detail. Many program transformations and refactorings are equivalences, i.e. refinements in both directions - the sense of which alternative is preferable remaining outside the direct semantic considerations. Attempts to fully integrate measurements of desirable non-functional properties, like running time or "bad smells", with this have not been convincing so far. This project would seek to apply modern sophisticated notions of refinement, which include ideas from probability and asymptotic theories, to shed new light on this.