Student summer internship projects, summer 2020

Implementing a library of optics

Mentors: Mario Roman and Pawel Sobocinski

Optics are used in functional programming languages as data accessors [1]. There exist multiple optic libraries of ranging complexity [2,3], but recent developments on optics [4,5] can be used to simplify and unify them. The goal of this project is to implement a practical library of optics using the new architecture and explore the expressivity of this new approach.

Implement the library in a functional programming language.
Improve the performance of existing prototypes [6].
Explore different optics as data accessors.

No prior knowledge is assumed. This project will suit a good programmer with experience in functional programming, who is also interested in learning the basics of category theory.

https://web.archive.org/web/20141219182332/
http://lukepalmer.wordpress.com/2007/07/26/making-haskell-nicer-for-game-programming/
https://hackage.haskell.org/package/lens
https://hackage.haskell.org/package/mezzolens
https://arxiv.org/abs/1809.00738
https://arxiv.org/abs/2001.07488
https://github.com/mroman42/vitrea/

Implementing games on graphs

Mentors: Elena di Lavore and Pawel Sobocinski

In economic game theory, network games are a model for situations in which players’ decisions are influenced only by their neighbors on a graph. In a recent paper Games on graphs: a compositional approach, we developed the theory to treat these kind of games compositionally.

The the project is to develop a software that implements the theoretical framework of this paper to compute the Nash equilibria of network games (e.g. the madness of the crowds or the parable of the polygons), given a formal description of the graph that the game is played on.

No prior knowledge is assumed. This project will suit a good programmer who interested in exploring game theory and basic category theory.

Implementing Accountable Automata

Mentors: Chad Nester and Pawel Sobocinski

Accounting tools represent a lucrative and important sector of the software industry. This project is about building tools for a compositional account of accounting processes. The idea roughly, is that two such processes can be combined in interesting ways to obtain a composite view of the accounts of an organisation from its individual parts. Applications of the approach also include smart contracts in cryptocurrency. The project is built on recent advances in the mathematics of open systems.

No prior knowledge is assumed. This project will suit a good programmer who interested in exploring classical accounting theory and basic category theory.

Basic computability theory with string diagrams

Mentors: Chad Nester and Pawel Sobocinski

In the early days of computer science, the theory of computable functions was developed in the language of set theory. From the perspective of a computer scientist this may seem to be unsatisfactory: the theory of sets and partial functions contains much that is not computable. Instead of taking only the computable parts of this not-very-computable setting, wouldn’t a theory of computation that stands on its own be preferable? There is a line of research into developing such freestanding theories of computation, including work on Turing categories.

The project is to experiment with doing elementary computability theory diagrammatically, using the string diagrams for a Turing category. We are interested not only in what is captured by the structure, but in whether or not using string diagrams to express it is a good idea. Does it make any classical results clearer? If so it could be a valuable teaching tool. Anything derived purely in the diagrammatic calculus will hold in Turing categories, contributing to the project of abstract computability described above.

This is a theoretical project. The student should have a strong interest and motivation to study abstract mathematics and in theoretical computer science. While no prior knowledge is assumed, the successful candidate is expected to start familiarising themselves with Odifreddi’s Classical Recursion Theory.

Diagrammatic logic evaluator

Mentors: Nathan Haydon and Pawel Sobocinski

In the 19th century the American polymath C.S. Peirce introduced existential graphs, a diagrammatic language for logic. Peirce was more than 100 years ahead of his time: mathematics has only recently cought up and we can now properly understand and study this language.

The project concerns a tool that will take a Peirce diagram and evaluate its semantics, its logical meaning.

No prior knowledge is assumed. This project will suit a good programmer who interested in exploring the concepts of classical formal logic and basic category theory.