Honours (UG4/MInf) Projects Suggestions

I believe in supervising projects I’m also passionate about, usually involving concepts that tie to advanced, cutting-edge research. The projects below mix programming language and computer science theory with some hacking. In my ideal project, theoretical concepts and developments would yield code that is clean, simple, and straightforward. While the project is entirely your responsibility, I believe you will best develop with close contact, meeting weekly during term or more often as the project requires. Great projects should be challenging, so as long as you are willing to put in the effort, I provide support in terms of guidance, discussion, explanations, and reading material.

• See the Degree Project Management Tool page for this year’s proposals. Please contact me even if only parts of the project sound interesting to you, and perhaps we could find a different project. You’re also encouraged to suggest your own projects!

Research prospects

The short duration of the Honours project (aboue 30% of your year) means you will likely not do enough research for a publication in a top-tier venue in my area. Such venues usually require 1-3 years of work, even with experienced researchers.

Past projects

Below are some of my past project suggestions and how they turned out.

Order completion in programming language semantics

Student: Thanakrit (New) Anutrakulchai

Models of programming languages with recursive functions often involve an order with a completeness property: certain least upper bounds exist. Usually, we want to make a model by taking the syntax of the language and quotienting it by semantic equivalence. This quotient doesn’t have enough least upper bounds, so we need to add them somehow. In this project, you will investigate an ideal-completion construction that adds the missing upper bounds. You will use this construction to create an ordered model for a simplified recursive programming language, and use it to reason about concrete models of interest.

• Lecture notes on Denotational Semantics by Marcelo Fiore

Difficulty: Very Hard

Completion Criteria

• Basic

1. Understand and explain the context (you will need to learn some domain theory in the process).
2. Prove the required properties of the completion.
3. Use it to construct a model out of the syntax.

• Extension

1. Derive the adequacy approximation relation by relating a syntactic model with a concrete model.
2. Reconstruct the completion using free enriched cocompletions.

Desirable Skills

• Background in order, category, or domain theory.

Essential Skills

Mathematical maturity, evidenced by extensive mathematical background (for example, a joint mathematics degree), or a previous theoretical project (for example, an undergraduate dissertation or a theoretical internship).

Towards strong relative pseudomonads

Self-proposed project by Franz Miltz

Abstract

Synthetic measure theory uses commutative monads to develop an entirely categorical language of measures and integration. This language has proven practically useful in the development of higher-order statistical programming languages.

There is another purely categorical notion of integration: coends. Certain coends arise from the presheaf construction, a monad-like structure that fails to be a model of synthetic measure theory for several reasons. There are multiple ways in which one could attempt to fix these problems.

In this report, we make a start at defining a strong relative pseudomonad that would be suitable as the backbone of an extended synthetic measure theory. At each step, we show how the presheaf construction gives rise to the required structure and how this structure satisfies the necessary axioms.

Unfortunately, the strength of a monad does not lend itself to being generalised to relative pseudomonads. We are thus neither able to give a complete definition of a strong relative pseudomonad nor do we manage to extend synthetic measure theory to admit the presheaf construction as a model.

Note

The week after Franz submitted his dissertation, Andrew Slattery uploaded to the arXiv an independent and fuller development. Check it out!

Higher-order measure theory with quasi-Borel spaces

Student: Andrew Ricketts

The foundations of statistical modelling are based on measure theory, based on the concept of an event. A recently-proposed alternative are quasi-Borel spaces, based on the concept of a random variable. But unlikely the century-old measure theory, quasi-Borel space theory is under 5 years old, and so require further mathematical development.

In this project, you will investigate possible new results in quasi-Borel space theory.

• A convenient category for higher-order probability theory (http://dx.doi.org/10.1109/lics.2017.8005137)
• Denotational validation of higher-order Bayesian inference (http://dx.doi.org/10.1145/3158148)
• Factorisation Systems for Logical Relations and Monadic Lifting in Type-and-effect System Semantics (http://dx.doi.org/10.1016/j.entcs.2018.11.012)
• Kallenberg, O., Foundations of Modern Probability, 2nd ed. Springer Series in Statistics. (2002). 650 pp. ISBN 0-387-95313-2
• Probability with Martingales (http://dx.doi.org/10.1017/cbo9780511813658)
• Random Measures, Theory and Applications (http://dx.doi.org/10.1007/978-3-319-41598-7)

Difficulty: Very Hard

Completion Criteria

Basic

• Survey the theory of quasi-Borel spaces
• Compare existing results with their measure theoretic counterparts

Advanced

• Extend the theory of quasi-Borel spaces

Desirable Skills

Experience with category theory, measure theory, or modern statistics.

Essential Skills

Mathematical maturity, evidenced by extensive mathematical background (for example, a joint mathematics degree), or a previous theoretical project (for example, an undergraduate dissertation or a theoretical internship).

Theory and implementation of ordinal diagrams

Student: Julius Gaidys

The ordinals are given by the following seemingly inductive definition: every set of ordinals has a least upper bound; and every ordinal has an immediate successor ordinal. A fundamental property of the ordinals is that they are /well-founded/: every strictly decreasing sequence of ordinals is finite. Ordinals have an arithmetic: they can be added, multiplied, and exponentiated infinitely many times. So ordinals reify the concept of ‘a terminating process’, and give us a calculus of such processes, so long as the ordinal we associate to each process decreases with the process’s evolution. They are also a foundation for inductive definitions.

An /ordinal notation system/ is a (countable) syntax together with a decision procedures LESS_THAN with these properties: 1. Every term represents a unique ordinal. 2. LESS_THAN decides for every two terms whether they are equal to, less than, or greater than, each other, as the ordinals they represent. 3. If a term represents an ordinal, every ordinal below this ordinal has a term representing it.

So an ordinal notation system lets us represent a fragment of the ordinals, for example, to store in data structures and pass around as values inside a formal system as a witness that a given process terminates. The least upper bound of the ordinals represented by a given notation is called its /proof-theoretic strength/. By using systems with high strength, we can support the foundation of logical and formal systems of high expressive power.

Takeuti’s /ordinal diagrams/ are an ordinal notation system with high proof-theoretic strength. In this project, you will help simplify and explain this system in several complementary ways: implementing them and their decision procedure as data structures and operations on them; establishing their meta-theory; and apply them in termination proofs.

• Mitsuhiro Okada and Gaisi Takeuti. On the theory of quasi-ordinal diagrams. In Logic and Combinatorics (Arcata, CA, 1985), volume 65 of Contemp. Math., pages 295–308. Amer. Math. Soc., Providence, RI, 1987.
• Dershowitz, Nachum. “The Ordinal Path Ordering.” Informal Proceedings of the 13th International Workshop on Termination (WST 2013, Bertinoro, Italy). 2013.
• 10.1007/978-3-319-94205-6_9

Difficulty: Very hard Search tags: ordinals, termination, proof theory

Completion criteria

Basic

• Implement an ordinal diagrams notation system.
• Establish the meta-theory of it (well-ordering)

Extensions, depending on the student’s interests:

• Develop the arithmetic of ordinal diagrams
• Find modular proofs for the meta-theory
• Apply ordinal diagrams to prove a system terminating

Essential skills and knowledge

1. Mathematical/theoretical computer science maturity (e.g.: you can formulate mathematical hypothesis and prove them). (2) Basic coding skills.

Desirable skills and knowledge

1. Experience with ordinals and transfinite induction. (2) Experience with transfinite combinatorics/Ramsey’s theorem. (3) Experience with termination proofs.

Handling Transparent Code Migration

Student: Oscar Key

The details of implementing distributed protocols, algorithms and programs can be quite hairy, as we need to send code and data between end-points. Mobile computation is an approach to distributed programming where a program works by migrating from one host to another. The migration is called transparent if the execution state of the program is preserved before and after the migration. Concretely, we have a “go” statement that lets us switch to a different machine and continue execution there. For example:

for host in network
  go host
  update_dns_table("CL", 128.232.0.20)

Two crucial components of transparent code migration are value marshalling (sending values to a different end-point), and thunkification (reifying computations into marshallable values).

The goal of this project is to utilise a couple of programming language techniques, type-directed partial evaluation and effect handlers, to provide a lightweight transparent code-migration library. Then use the language’s existing libraries and features to demonstrate a series of nifty distributed programs, or a big single distributed application. One such example would be to extend Kiselyov’s file server to a distributed file system.

Little work has been done on extending an existing runtime systems easily, and this projects builds on Sumii’s work this project builds which uses delimited continuations. One reason we might want to write migrating code is to have some computational effects (state changes, exceptions, I/O) at different hosts, which the Sumii’s approach doesn’t deal with, but effect handlers are well-suited for.

Your profile: eagerness to learn advanced functional programming tools and techniques (e.g., Haskell, monads, delimited continuations, effect handlers, type-classes, zippers), and acquire new programming abstractions and use them in exciting ways.

Related courses that you have taken or will take this year: semantics, types, concepts in programming languages, and concurrent and distributed systems.

Source-Level Compile-Time Optimisations For Java

Self proposed project: Chris Kitching

Graphical and Polynomial Combinations of Algebraic Theories for Semantics

Outcome: This project attracted some attention from prospective students, I fleshed out a more concrete outline, which made me realise this project can be even more fun than I expected. As no student ended up choosing this project, I decided to do it myself. I will be presenting the webtool I produced at the upcoming 3rd ACM SIGPLAN workshop on higher-order porgramming with effects, co-located with the 19th ACM SIGPLAN international conference on functional programming.

(Based on pages 34-38 of Hyland, Plotkin and Power’s Combining Effects: Sum and Tensor.)

Defining the meaning of programming languages using denotational semantics is particularly useful for optimising compiler design. When constructing denotational semantics for languages with computational effects (such as state, exceptions, I/O, and non-determinism) two algebraic operations emerge as useful: the sum of two theories and their tensor. These operators lead to a description of algebraic semantics as polynomials in theories. However, choosing the exact order in which to perform these two operations on the theories at hand is non-trivial. Arranging the data as a graph leads to a more intuitive description: each semantic theory corresponds to a vertex, and two vertices are connected iff the corresponding theories should commute. The graphical notation is strictly more expressive than the polynomial notation. Linear polynomials enable an extraction of the monadic semantics using monad transformers, which are already usable by functional programmers.

The goal of this challenging project is to provide tools for investigating algebraic semantics. In particular, studying and implementing Hyland et al.’s various algorithms:

• deciding whether a given graph description has a corresponding polynomial description and extracting this polynomial; and
• deciding whether a polynomial is linear and extracting the monad transformer stack corresponding to a linear polynomial.

For a successful project, the student would need to understand the algebraic properties of these polynomials, their connection with the graphical notation, and the various algorithms involved. The student would also need to implement graph algorithms and data structures for syntax.