Student projects

Programming projects

(All preferably in a functional language such as Haskell, Lean, Idris, OCaml, Erlang, …)

• Basic Matrix server and bot implementations (without encryption), see the protocol specification (draft).
• Basic ActivityPub or Nostr server/bot implementations.
• 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
• A verified implementation of Haskell, similarly to how CakeML is a verified implementation of ML.
• 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.
• Create trace comonads – apply a similar straty to that of creating game comonads to constructions arising in automata theory.
• 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, …)