Thesis Topics from Chad Nester

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. Interested students are encouraged to contact me at nester@ut.ee.

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]. 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. Interested students are encouraged to contact me at nester@ut.ee.

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. Interested students are encouraged to contact me at nester@ut.ee.