Thesis Topics from Chad Nester

The lambda calculus is a simple notation for functions and application, and constitutes one of the earliest and most successful notions of computable function [1]. In particular, the lambda calculus admits various sorts of fixed point combinator, which may be used to model recursion.

One way to understand the lambda calculus is in terms of operads. Specifically, the lambda calculus can be seen as the initial semi-closed cartesian operad [2]. From this, we may use standard category-theoretic techniques to obtain a closed monoidal category. I would like to know whether or not this monoidal category is traced, which seems quite likely [3].

Writing a thesis on this topic will involve becoming intimately acquanited with the lambda calculus, and with different sorts of fixed point combinators therein. If we make good progress you may eventually have to learn some elementary category theory, in particular the theory of traced monoidal categories.

Combinatory logic is a simple formalism that captures the computable functions, not unlike the lambda calculus [1]. Combinatory algebras are models of combinatory logic, in the sense of universal algebra. There are a number of questions concerning combinatory algebras that I would like to know the answer to.

For example, a combinatory algebra is called extensional if, loosely speaking, elements with the same "behaviour" are equal. A natural question is: does every combinatory algebra have an extensional completion? That is, given a combinatory algebra, can we construct an extensional combinatory algebra from it, preferably with nice mathematical properties.

Separately, every combinatory algebra defines a category of computable maps [2,3]. I would like to know when this category has equalisers. In particular, I am interested in internal categories that live in the category of computable maps of some combinatory algebra, and the category of computable maps must have equalisers for this to make sense.

Writing a thesis on this topic will mostly involve working with combinatory algebras, and the specifics will depend on what precisely we end up studying. It is likely that this will involve some category theory, but it need not.

The notion of binoidal category was introduced as an intermediate step in the definition of premonoidal category [1], which is one approach to the semantics of effectful computation. The structure of a binoidal category consists of two "halves". Throwing one of these halves away, we arrive at something that we might call a "noidal category".

There seems to be a connection between noidal categories and stack machines, which are state machines that manipulate a persistent stack, typically according to lists of program instructions. Examples include the SECD machine [2] and the Krivine machine [3]. It would be interesting to explore this connection.

Writing a thesis on this topic would involve getting acquainted with a couple of different stack machines, and with the proposed notion of "noidal category", and with a bit of elementary category theory.

Elgot Categories are an approach to the categorical semantics of simple imperative programming languages [1]. They are closely related to Abacus Programs, which are a simple model of computation [2], which give the initial Elgot category.

While it is possible to construct an initial Elgot category of abacus programs, the construction is ugly. Goncharov's while monads suggest an alternative approach [3]. It should be possible to obtain an equivalent definition of Elgot categories in the style of while monads. Hopefully, this will lead to an alternate presentation of the initial Elgot category in terms of a "While" language that is less ugly than its presentation in terms of abacus programs.

A further step could be to study the relationship of the dentational semantics for "While" programs given by Elgot categories to their operational semantics.

Large programs are almost always divided into modules. This has a number of benefits and is supported in some form by all industrial-strength programming languages. Before a program is run its modules must be linked. In principle this can be done either statically, at compile time, or dynamically, at runtime.

Approaches to programming language semantics tend to focus on monolithic programs, and in spite of their ubiquity there would seem to be surprisingly little theory concerning program modules and linking. The goal of this project is to develop such a theory.

One approach that seems particularly promising is to model modules and linking via the "Int construction" [1] (also known as the "geometry of interaction construction"). It would seem that applying the Int construction to a traced cartesian monoidal category results in a model of "statically linkable" program modules. Dually, applying the Int construction to a cocartesian monoidal category results in a model of "dynamically linkable" program modules. Here the original (cartesian or cocartesian) monoidal category should be thought of as a model of monolithic programs in some language.

Writing a thesis on this topic will likely involve learning a bit of category theory (esp. traced monoidal categories and the Int construction) and how it can be used to model (simple) programming languages. One would then, with my guidance, proceed to develop a categorical theory of program modules and linking. The ideal outcome is a simple, general notion of program module that can be used to equip a wide range of "monolithic" programming languages with a module system.

You are of course very welcome to propose another approach to the semantics of program modules and linking.

String diagrams are way to represent morphisms of monoidal categories graphically [1], and are a useful tool for reasoning about such morphisms. While string diagrams are easy to work with on paper, working with string diagrams on a computer is rather painful.

The proposed project is to develop software tools for working with string diagrams.

In particular, I have a prototype implementation of a tool that allows the user to type string diagrams over a given monoidal signature using the keyboard, storing the result as text, which can they be parsed and displayed to obtain the original diagram. It would be nice if someone made a cleaner version of this, and especially nice if it had editor integration with, in particular, Emacs. Other directions include support for more general forms of string diagram, as in e.g., [2].

The project does not need to be specifically about the idea described above, and I would be happy to supervise work on other projects in this area. Interested students are encouraged to contact me at nester@ut.ee

The simply-typed lambda calculus is perhaps the simplest typed functional programming language. It has been studied extensively, and often serves as a testbed for new ideas in programming language research (see e.g., [1]).

The goal of this project is to extend the simply-typed lambda calculus to support certain typed interaction primitives, in the sense of interaction with an environment. For example, when a program reads from the standard input or writes to the standard output it is engaged in this kind of interaction.

Specifically, a novel approach to the semantics of program interaction has recently been proposed in a series of papers [2,3,4]. It should be relatively straightforward to apply these ideas to the simply-typed lambda calculus, resulting in a simple "interactive" programming language with a satisfying formal semantics.

How to approach this kind of interaction is one of the larger open questions in programming language semantics, and there would likely be a good amount of interest from the wider research community.

A great deal of confusion surrounds the idea of a "smart contract". A reasonable informal definition of smart contract is "a process with a bank account". Through creative interpretation of the words "process" and "bank account", existing smart contract infrastructure may be viewed in these terms.

The goal of this project is to arrive at a formal notion of smart contract. A particularly promising approach is to apply the theory of situated transition systems [1]. The formal notion of process is a span of reflexive graphs, as in the work of Walters et al. [2]. Monoidal categories are used to model the resources (e.g., money) a process is in control of [3], with the relationship between the two being a sort of coherent labeling of the edges in the involved graphs.

Writing a thesis on this topic will involve learning about the theory of situated transition systems and using it to model common smart contracts. Another possible direction is to develop software tools for working with situated transition systems.

A good theory of smart contracts (in the "process with a bank account" sense) is likely to have numerous applications in the financial technology sector.

In the study of programming languages, abstract machines are a method of specifying the operational semantics of programs, particularly for languages based on the lambda-calculus. See for example the SECD machine [1], the Krivine machine [2], and the Functional Machine Calculus [3].

Curiously, most abstract machines can be viewed as partial monoid actions (see e.g., [4]) The elements of the monoid are the instruction sequences for the machine in question, and the effect of these instruction on the machine state describes the action.

The project is to study abstract machines for, say, the lambda calculus from this perspective. One imagines that significant (informal) differences between abstract machines will induce corresponding (formal) differences between partial monoid actions.

Writing a thesis on this topic will involve spending a substantial amount of time with both different abstract machines and with the relevant concepts from abstract algebra. You must be comfortable with, for example, mathematical proofs.