Projects and projects-to-be

There is so little time I can spend on these things: if you're interested in working on something in the list below, please let me know how I can support you.

If there are on or more *** in front of an item, it means that I'm currently more or less actively working on it, or that I have some tangible results already.

This list is under construction. In particular, I will be adding more detailed descriptions, and links to related sites. In the future, each of these will probably have a separate page.

Mathematics

• *A proof of a basic theorem in topology. In a topology course at university, I encountered a difficult-to-understand proof of a basic topology theorem. It kept bugging me, until I sat down and designed a calculational proof. Then it turned out that the proof from the book was lacking in a number of respects. I would like to write down that proof, and publish it here and/or as an article.
• AUQL: Algebraic Unified Quatum Logic. Normal Megill with his Metamath project/program set me on the trail of this logic. I might take some time to get to know it better.
• Alternative Set Theory. Invented by Vopenka, and evangelised by other mathematicians from Prague. A set theory that is meant to be more realistic than the usual Zermelo-Fraenkel set theory. They do this by working only with finite sets, and then introduce the concept of a 'semiset' which allows the introduction of infinity in a different way. The best introduction is Vopenka's little blue book of the same name.

  Mathematics & Engineering

• A translation of EDM (Engineering Data Model) in logical terms. A friend of mine (Roel Schipper) worked together with Scott Chase and Charles Eastman from UCLA on an implementation of EDM. At that time I thought that it should be easy to use predicate logic instead of the language that EDM offers. That was some time ago, but I still have the EDM documentation lying around, and I should really give this a try.

  Mathematics & computer science

• *Program-refining data. The refinement calculus is a formalism for reasoning about (sequential, structured) programs. 'Data refinement' is a separate refinement technique; I've found a way to integrate it neatly into program refinement. Some years ago I started to write an article about this; I never had time to finish it.

  Calculational proofs

• ***[Calculational solutions to logical puzzles.] Apart from the solutions published on this site, I would like to write an article that uses logical puzzles to showcase calculational proofs.
• ***A calculational proof of the Master theorem. After being challenged on sci.math, I worked on a calculational proof of this theorem (from "Introduction to Algorithms" by Cormen, Leiserson, and Rivest). The article is now about 80% done; I'm hoping to find the time to finish and submit it to some journal.

  Calculational proofs & software

• Metacalc: a calculational proof tool for Metamath. Metamath is a small virtual machine for proof verification. It is also a tool that implements that VM, and offers some support in the construction of proofs. However, proof construction is not easy, and the resulting proofs (which are inference trees) are often not easy to read. I would like to build a frontend that allows viewing and constructing Metamatch proofs as calculational proofs; I already have some ideas on how it could work.

  And I have a bit of implementation as well; see [Hmm].

• A JSP tag library for calculational proofs. Something like the 'proofviews' library that Jim Grundy wrote, but now in Java for use in JSP pages.

  Software

• A good open source Java CommandLine class. For a project at work I wrote a CommandLine class, to parse command line arguments to a Java program. But that version has at least four deficiencies: (1) its interface is too complex; (2) its implementation is too complex; (3) it lacks a number of useful features, such as equivalence of long and short options, and the automatic generation of a 'usage' message; (4) and it is not open source.
• A keyboard GUI. With the introduction of the GUI, the guys at Xerox also introduced the mouse. So when we think of a GUI, we think of a principally mouse-driven user interface, where keys are sometimes useful too. (Hence the term 'keyboard shortcuts'.) In these times of RSI, I would like to design a GUI that can be completely and consistently driven through a keyboard. (Optionally with 'mouse shortcuts'.) This would probably make it very popular with programmers, system administrators, UNIX- lovers, and similar races.

  Software & Websites

• [Memostor]. A Wiki-clone that I'm working on, every now and then. (More then than now.) Uses JSP and JDBC (because I want to learn more about those), and 2D-text for text formatting.

  Software & Tools

• **['same': the opposite of 'diff']. An open source tool for finding identical lines in a set of files. Similar to 'duploc', but without a visualization mode, and optimised for performance.
• *2D-text. The WikiWikiWeb and its numerous clones all have a very simple input , in plain ASCII, that is automatically translated to nice-looking HTML. However, the formats that they use are very ad hoc. I've been thinking about a that fulfills at least the following requirements: (1) The two-dimensional structure of the input (i.e., indentation) determines the layout; (2) the input itself should itself be reasonably readable; and (3) invisible characters (spaces at the end of a line, tabs vs. spaces) are irrelevant to the layout. I call that '2D-text'.

  Interactive Fiction

• Interactive fiction. I really would like to try my hand on some. Since English is not my native language, I would prefer to do it in Dutch. Perhaps together with my writing sister-in-law Nellie. (Then again, perhaps I should focus on building tool support for IF; I'm a tools builder, not a writer.)

  Interactive Fiction & Software

• Jlk: Java-based Glk. Specification of such a beast. It should be able to create a Servlets-implementation of Jlk, so that Interactive Fiction written in Java can easily be published on the Web.
• A universal IF-player which stores a history tree. Dubbed by someone 'the many-worlds interpretation of Interactive Fiction'. Implemented in Java using Jlk, of course. The implementations of the separate virtual machines are modules that can be plugged in to a generic frontend. (And it should be able to plug in IF written in native Java, as well: just implement a number of interfaces that I will provide.)

  Interactive Fiction & Software & Programming Language Design

• IFTalk. A Smalltalk dialect especially suited for programming Interactive Fiction. Based on the concept of 'predicate dispatching', which should make implementations of IF software more modular. I would like to make an implementation that compiles to Glulx or Z-code.

  Programming language design

• **Adding attributes to Haskell. I designed Hattr, an extension to the functional programming language Haskell which allows direct expression of attribute grammars. I had submitted an article to the Journal of Functional Programming, but it was rejected. I probably will publish it here. I have the outline of a prototype implementation. I don't know whether I'll have the courage to continue :-)

  Writing

• Nanofiction. I really would like to try some. It can't be difficult. I mean, how difficult can it be to write a story of 55 words?

Changes to projects.html:

Fri Oct 21 06:25:37 MEST 2005  Marnix Klooster <myfirstname.mylastname@gmail.com>
  * Added item about Hmm.

Sat May  7 10:00:13 MEST 2005  Marnix Klooster
  * Minor: make 'tidy' complaints go away.

Sat Oct 30 12:38:39 MEST 2004  Marnix Klooster
  * Move from CVS to darcs: do not show the CVS date anymore.

Sat Oct 13 18:07:14 MEST 2001  marnix
  * first HTML file translated to use m4 HTML generation

Wed Sep  5 21:20:00 MEST 2001  marnix
  * Made explicit that last changed date is in GMT

Wed Sep  5 21:08:51 MEST 2001  marnix
  * Now 'last changed' is on its own line

Wed Sep  5 10:10:47 MEST 2001  marnix
  * Added date last changed

Wed Sep  5 08:50:24 MEST 2001  marnix
  * Initial revision