# Student projects

## Programming projects

(all preferably in Haskell, Erlang, Idris, ML, OCaml, Scheme, Fennel, …)

- Basic Matrix server and bot implementations (without encryption), see the protocol specification (draft).
- Basic ActivityPub server implementation.
- Implementation of IndieWeb technologies: indieauth, micropub, webmentions, …
- NeoVim plugins:
- Haskell Treesitter plugin for code manipulation
- Agda plugin for interactive theorem proving, using the Agda Haskell library.

- New git-merge algorithm sensitive to minor line changes.

## Theoretical projects

Game comonads

- A survey of categorical properties of the base category that transfer to the category of coalgebras for a comonad.
- Explore the relationship between containers and game comonads.
- Explore the relationship between coeffects and game comonads.
- Can coinduction from the theory of universal coalgebra be used to simplify some known proofs with game comonads?
- Bisimulation up-to and coinduction up-to in the setting of game comonads.
- Explain the relationship between distributive laws of the powerset comonad and list comonad or the list monad and list comonad and the hypergraph comonad. Similarly, for a distributive law of the product and list comonad leading to the pebble comonad.

Topology and duality theory

- Choice-free duality theory for distributive lattices.
- Canonical extensions of frames.
- Probabilistic relational structures via duality theory, with applications to the theory of structural limits.

Formalisations

- Agda/Lean/Coq formalised proofs of standard theorems of game comonad, pointfree topology, or even algebra and category theory.

Other

- survey of theoretical properties of dependency systems (contrasted with the ones used by programming languages today, e.g. in Node, Rust, Java, Haskell, OCaml, …)