Author Archives: Thomas Strathmann

Using Qucs for filter design

Qucs, short for Quite Universal Circuit Simulator, is as the name suggests a simulation package for electronic circuits. It’s free and sports a nice graphical schematic capture interface. One of its many nice and useful features is the ability to … Continue reading

Posted in Electronics, Tools | Tagged , | 3 Comments

WordPress blogging in LaTeX

Just found an interesting resource about blogging in LaTeX using WordPress. Eric Finster at Curious Reasoning has put together a Python script that allows you to prepare blog posts in LaTeX and convert them to the proper format. Might come … Continue reading

Posted in Tools | Tagged , | Leave a comment

Beginning Ltac

One of the strong points of Coq is its powerful proof automation facility embodied in the tactic language . Instead of having to write new tactics in ML, compiling them, and jumping through all sorts of hoops in the process, … Continue reading

Posted in Coq | Tagged | Leave a comment

How to draw commutative diagrams in LaTeX with TikZ

Sooner or later everyone who uses LaTeX to typeset documents containing maths will encounter the problem of how to draw commutative diagrams. There are many packages, some general purpose other specialized for the task. An excellent survey of some of … Continue reading

Posted in Mathematics, Tools | Tagged , , , | 24 Comments

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