An experiment in typing up my various notes (using Markdown) instead of writing things out by hand. Not quite as polished as a blog, but in the same vein.
Different research ideas are put in its own file. Right now, there are notes on:
- Dependence as a concept.
- Composite Levels as a way to say that we're pairing things up that belong in different universes, without commiting to them living in the same universe.
- Generic Programming Revisited will tell the story of how various flavours of generic programming are related.
- Module System explores what a module system is / ought to be, and then tries to make that more precise for Agda. For the curious: most likely what's needed is a parametrized namespace system, rather than a full blown module system.
- InvisibleMath is Andrej Bauer's wonderful term for the mathematics that is implicit in "paper math" but that is often explicit in formalized mathematics. This is indeed an opportunity afforded by proof assistants that reveals something about the process of mathematics that should be leveraged some more.
As a means to not forget stuff, I also jot down research ideas. These are not so much centered around wished-for results, but rather they are a collection of questions that, once answered, ought to yield interesting results.