Monthly Archives: January 2011

Another script font for LaTeX

Sometimes it’s nice to have an extra script font available to make distinctions between different kinds of objects clearer. One such font is Ralph Smith’s Formal Script (see here for the TeX Catalogue entry) which is provided by the mathrsfs … Continue reading

Posted in Tools | Tagged , , | Leave a comment

Category Theory Video Lectures

Edsko de Vries of Trinity College Dublin has created a very useful overview of the series of lectures on category theory by Eugenia Cheng and Simon Willerton that has been available on Youtube for quite some time. So, if for … Continue reading

Posted in Mathematics | Tagged | 1 Comment

Doepfer MCV4 MIDI to CV interface editor in Max

A little Max patch for changing the parameters of a Doepfer MCV4 MIDI to CV interface I made a while ago. It’s not extensively tested, but seems to work so far. The user interface is in German, but I guess … Continue reading

Posted in Music Software | Tagged , , , | Leave a comment

How I use git Part 2: Emacs integration

The strangest things happen. Once I was a GNU/Linux user who spent most of the time staring at a framebuffer console and used vim exclusively. Today I use Mac OS X and Aquamacs most of the time (although I still … Continue reading

Posted in Tools | Tagged , | 1 Comment

The Maybe monad in Coq

The Maybe monad is pretty useful whenever you’re dealing with partial functions, especially in a language like Coq (or rather Gallina if you want to be exact) which requires all functions to be total.

Posted in Coq, Haskell | Tagged | 8 Comments

Coq Syntax Highlighting Test

A test case for Coq syntax highlighting in GeSHi (for the WP-Syntax plugin). Inductive nat : Set := | O : nat | S : nat -> nat.   Inductive fin : nat -> Type := | FO : forall … Continue reading

Posted in Coq, Tools | Tagged , , | Leave a comment

Partiality is an effect

In languages like Coq where all computations must terminate and only total functions are allowed it would still be nice to be able to express non-terminating computations. While searching for solutions other people had come up with I stumbled across … Continue reading

Posted in Coq | Tagged , , | Leave a comment

WordPress + SQLite

The one thing that really kept me from just installing WordPress and playing around with it was that it required MySQL to run. I don’t need a full-blown RDBMS on my server and I certainly don’t need MySQL (in the … Continue reading

Posted in Tools | Tagged , , | 3 Comments

How I use git

After many years of using SVN, my current revision control system of choice is git. It makes distributed and offline work a breeze, so I don’t always have to log in in to a remote repository when I want to … Continue reading

Posted in Tools | Tagged , | Leave a comment

Definition of a monad

This rather rendundant post serves as a test case for the WP LaTeX plugin. A monad on a category is given by an endofunctor  and two natural transformations: such that the following two diagrams commute:

Posted in Mathematics | Tagged , | Leave a comment