-
Recent Posts
Archives
Categories
Meta
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
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
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
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
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.
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
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
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
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
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: