For Students
Letters of reference
If you’re thinking of asking me for a letter of reference (which I am generally happy to write), please read this guide.
Projects
I’m always looking for motivated students who are interested in pursuing an independent study or research project. Below are some ideas which I’d love to have students work on. Many of these may be appropriate as either a senior project/thesis or as a summer research project.
Recreational mathematics and computation
These projects would be particularly appropriate for students interested in both computer science and mathematics.
Strategies for nim-like games with extra losing conditions
See this blog post (and the preceding posts it links to) for background. The goal is to understand various families of impartial two-player games, and how optimal strategy is affected by the introduction of arbitrary extra losing conditions.
Visual communication and embedded domain-specific languages
Many of my ideas for research projects in this space center around diagrams, a domain-specific language, embedded in Haskell, for creating vector graphics. If you are generally interested in visual communication or domain-specific languages, I encourage you to play around with it—there are many other good ideas for projects we could come up with, other than the specific ideas listed here.
Automatic generation of simplified APIs for embedded domain-specific languages in Haskell.
Diagrams is highly flexible, but suffers from the problem that its type signatures are hard for beginners to understand, due to their generality. The idea behind this project is to create a tool for automatically generating simplified (but less flexible) versions of the API for use by beginners. Ideally this will have applications to other embedded domain-specific languages beyond just diagrams.
A bidirectional GUI/programming environment for creating and editing vector graphics.
The idea is to create a GUI that allows not only writing diagrams code and immediately seeing the resulting image, but also directly manipulating the image (e.g. by dragging or resizing things) and have it update the code. There are a lot of interesting challenges here, and a wide range of possibilities—from simple things like drag-to-reposition, to more complex things like automatically inferring relationships among components of a diagram, and applying “example” gestures appropriately to entire classes of components.
Combinatorics and formalized mathematics
A formally verified, functional implementation of Sawada’s algorithm.
Given a multiset of objects (say, four red beads, two blue beads, and three yellow beads), can you list all the distinct “necklaces”, i.e. circular arrangements, you can make from them? Note that two necklaces are considered the same if they are just rotations of each other.
This is actually a nontrivial problem. There is a nice paper by Joe Sawada giving an algorithm that solves it efficiently, based on some interesting mathematics. I would like to develop an implementation of the algorithm in Agda and formally prove it correct. I expect this will yield new insight into the algorithm and the mathematics underlying it.
A previous research student made some good progress but there is still lots of work left to be done.
Translation (from French) and commentary on a paper by André Joyal.
Joyal’s classic paper Une théorie combinatoire des séries formelles, which introduced the theory of combinatorial species, is a really amazing piece of work, chock-full of interesting combinatorial insights. Unfortunately (1) it is in French and (2) you have to already know a good deal of combinatorics and other things in order to fill in the gaps and make sense of it. My goal is to produce an English translation, along with additional commentary and illustrations to help make it accessible, to, say, the average undergraduate mathematics or computer science major.
There are many ways a student could help with this project, from producing the translation itself, to helping create illustrative diagrams, to writing and editing the commentary. This is not really “research” per se, but it would be a great service to the mathematics and computer science communities, and would be a great way to bootstrap your way into some real research. It would be helpful if you know some French, but not essential—I don’t know French at all, but reading mathematical French with the help of Google translate is not too hard. All you really need is a desire to learn some interesting combinatorics with applications to computer science.
Independent study topics
Here are some suggested topics on which I’d be willing and able to supervise an independent study. Come talk to me if you’re interested (better yet, bring some friends).
Advanced functional programming
Applicative and traversable functors, monads, generalized algebraic data types, lenses, continuations, coroutines, dependent types… there is an infinitely deep rabbit-hole of amazing topics to explore, which are simultaneously of theoretical and practical interest. For anyone who is already sold on the value and beauty of functional programming and wants to become a true FP ninja.
Proof assistants
The theory and practice of computer proof assistants such as Coq, Agda, ACL2, and Isabelle, among others. Such systems/programming languages assist you in writing formal mathematical proofs, and certify that your proofs are correct. They can be used for many purposes, from formalizing pure mathematics to verifying the correctness of processor designs.
Category theory
Category theory is a beautiful and abstract branch of mathematics with applications to computer science, logic, combinatorics, algebra, physics, and topology, to name just a few. In a nutshell, it can be thought of as the study of “structure-preserving maps”, or homomorphisms. Such structure-preserving maps—connections between different objects or different areas of mathematics that reflect the inherent structure of one into the other—are really at the heart of what mathematics is all about, and what makes it so much fun (in my humble opinion).
Combinatorial species
Combinatorial species are what you get when you put category theory and combinatorics in a blender and drink the delicious result. (Note, however, that you can get quite far in studying combinatorial species with a decent background in combinatorics but zero background in category theory.) (Also, putting math in a blender should only be done by trained professionals using proper safety equipment.) They provide a unified framework for doing a lot of enumerative combinatorics, and in particular give a unified perspective on generating functions.
Homotopy Type Theory
Homotopy type theory is a hot new area at the intersection of computer science and mathematics (see this recent CACM article). It makes formal and rigorous something mathematicians have informally adhered to in practice for a long time: that isomorphic structures are interchangeable. It can serve as an alternative foundation for mathematics, but one that (unlike set theory) is actually quite close to the way mathematicians really work, and is inherently computational.