Student projects

Below I list suggestions for potential student projects to do with me (e.g. final bachelor or master projects). The list is not set in stone and I welcome suggestions that are in some spirit similar to these listed below.

Programming projects

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

• Implementing distributed protocols:
  • 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, …
• Formal methods in software development:
  • Formally verified software e.g. with Hax to verify a Rust code in F*/Rocq/Lean.
  • A verified implementation of (mini)Haskell, similarly to how CakeML is a verified implementation of ML.
• New git-merge algorithm sensitive to minor line changes.
• 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
• Haskell–JavaScript interop projects, e.g.:
  • Port hyperapp and superfine to Haskell, to be used with GHCJS (ghc --js)

Theoretical projects

Programming languages

• Implement LambdaCalculus to WASM/WebAssembly compiler (using the S-expression representation to make things easier)
• Implement a Fully in-Place Functional Programming language, following the paper of the same name by Lorenzen, Leijen, Swierstra.
• Implement a simple typed programming language with an untyped FFI, using the blame calculus of Wadler–Findler from the paper “Well-Typed Programs Can’t Be Blamed”.
• Implement the Lazy Abstract Machine of Sestoft (for languages using a version of the `normal’ evaluation order)
• Implement the Linear Abstract Machine of Lafont
• Implement a simple dependent type language, following the description of Mini-TT by Coquand, Kinoshita, Nordström and Takeyama
• 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)

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