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.
- 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, …)