# Student projects

## Programming projects

(All preferably in Haskell, Lean, Idris, Erlang, 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. – probably build upon github:isovector/cornelis

- New git-merge algorithm sensitive to minor line changes.
- Port hyperapp and superfine to Haskell, to be used with
`ghc --js`

- Implement minimal Calculus of Constructions or a minimal functional language with linear types (e.g. by simplifying “Retrofitting Linear Types” due to Bernardy, Boespflug, Newton, Jones, and Spiwack)

## Theoretical projects

Game comonads

- A survey of categorical properties of the base category that transfer to the category of coalgebras for a comonad.
- Cops and robbers games versus coalgebra numbers.
- 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, …)