Peter Selinger's Software
This page contains pointers to some software that I have written. Some
of it is related to my research, and some of it is not.
Software related to my research
- Core Join Calculus Compiler (1996).
The core join calculus is an experimental distributed programming
language developed at INRIA Roquencourt near Paris. My implementation,
written in 1996, was the first one. It is somewhat crude. Written
entirely in C, it translates the join calculus to C in a single pass.
Unfortunately, the compiler is not very well documented. One of these
days, I'll re-implement it in ML and write something about the
abstract machine underlying it.
- Finite Lambda Model Applet (1998).
In my 1996 publication,
"Order-Incompleteness and Finite Lambda Models", I introduced a
notion of finite models for the untyped lambda calculus. This Java
applet allows one to construct such models and automatically calculate
the denotations of lambda terms in them.
- An Implementation of the Lambda-Mu-Nu Calculus (1998).
The lambda-mu-nu calculus is an extension of the simply-typed lambda
calculus with first-class control operators and disjunction types.
I studied the call-by-name and call-by-value semantics of this
calculus in my paper on
Control Categories. Here is an implementation, based on Krivine's
abstract machine. It is written in ML, and it translates the
lambda-mu-nu calculus to a fragment of C.
- PPL - A Prototypical Programming Language (with Ari Lamstein,
PPL is a PCF-like call-by-name prototypical programming language. It
was implemented by Ari Lamstein, as part of an Undergraduate Project
on Mathematical Foundations of Programming Languages at the University
of Michigan under my supervision. The purpose of the project was to
investigate the compilation of a simple programming language into
"assembly code", based on Krivine's abstract machine. Ari wrote a
Paper describing the language and its implementation in detail.
- Quipper - A Functional Quantum Programming Language (2013).
Quipper is an embedded, scalable functional programming language for
quantum computing. It provides, among other things, a high-level
circuit description language, extensible quantum data types,
programmable circuit transformers, extensive libraries of quantum
functions. Seven non-trivial quantum algorithms from the literature
are included as worked examples.
- Newsynth - Single-Qubit Approximate Synthesis (2013)
ancilla-free Clifford+T approximation of z-rotations", Julien Ross
and I described an efficient algorithm for single-qubit approximate
synthesis in the Clifford+T gate set. This Haskell package provides an
implementation of the algorithm in the form of an easy-to-use
executable program. The package also provides a library of various
algorithms for exact and approximate synthesis of quantum circuits
over the Clifford+T gate set.
Interactive Web Demos
- Lagrangian Mechanics Applet (1999)
This applet was written as an illustration for a differential
equations class that I was teaching at the University of Michigan. It
displays various animated finite-dimensional mechanical systems, such
as a double pendulum or a spring pendulum. The systems are simulated
in real time, based on the differential equations of Lagrangian
Mechanics. There are various physical parameters, such as masses and
lengths, which you can adjust.
- Non-linear Image De-noising in Fourier Space (2002)
This is a demo of an image de-noising algorithm that I have been
playing with. You can vary the amount of noise added to an image, and
you can also change the parameters that influence how the noise is
removed. The image is displayed both in (x,y)-space and in Fourier
TeX macro packages
- fitch.sty: Macros for Fitch-Style Natural Deduction (2002)
Fitch-style natural deduction is a system for writing proofs in
propositional logic and predicate logic. We use it in our logic
courses at the University of Ottawa. This is a set of easy-to-use
LaTeX macros that I wrote for making handouts for my classes.
- hexboard.sty: Macros for Hex (2022)
A set of LaTeX macros for typesetting Hex boards and positions.
- ccvformat: Tools for formatting a Canadian Common CV (2015)
The Canadian Common CV is an XML data format used by Canadian
researchers to enter their CV data once and for all. The ccvformat
tools can be used to format this data as human-readable HTML,
LaTeX, or PDF.
Some useful Unix/Linux tools
- phone: Managing Information on How to Dial Phone Numbers (1999)
This is a simple unix tool for figuring out the local way of
dialing a phone number. It is intended to be used in conjunction with
dialing scripts such as chat or wvdial, or in
conjunction with fax software or other kind of software that keeps a
database of phone numbers which may have to be called from different
- ccrypt: Encryption of Files and Streams (2001)
This is a replacement for the unix crypt tool. It is superior to
unix crypt in two respects: it provides much much stronger
cryptographic security, and it is free. ccrypt is based on the
Rijndael cipher, a 256-bit block cipher which underlies the
U.S. Government's Advanced Encryption Standard (AES). This cipher is
believed to be very secure.
- rip: Encoding CD's to mp3 Format (2000)
This is a shell script which provides a friendly, terminal-based user
interface for transforming entire CD's, or parts of CD's, to mp3
format. It acts as a convenient frontend to such tools as
cdparanoia (a first-rate free ripper) and notlame (a first-rate free
- hashfunctions: Hashes and Checksums of Files and Streams (2000, 2007)
This is a package of hash functions and checksum functions. It
contains fast implementations of SHA-1, SHA-256, and CRC-32.
- upprint: intelligent n-up printing (2001-2007)
The upprint package contains tools for better formatting of print
jobs. The psdim tool calculates optimal page placements for n-up
printing by looking at the rendered PostScript file. The lprwrap
tool is a wrapper around "lpr" with options for n-up and duplex
- Potrace: Transform bitmaps into vector graphics (2003)
A tool for tracing a bitmap, which means, transforming a bitmap
into a smooth, scalable image. The input is a portable bitmap (PBM),
and the default output is an encapsulated PostScript file (EPS). A
typical use is to create EPS files from scanned data, such as company
or university logos, handwritten notes, etc. The resulting image is
not "jaggy" like a bitmap, but smooth. It can then be rendered at any
- farsiweb: generate Farsi webpages (2005)
Farsiweb is a simple tool for generating web content in Farsi, the
language of Iran. Farsi is written using the Arabic alphabet with some
additional letters. Farsiweb works by reading a file containing ASCII
transliterations of Farsi content, and translating this to
HTML-encoded Unicode suitable for display on web pages.
- MD5 collision demo (2006)
In March 2005, Xiaoyun Wang and Hongbo Yu published an article in
which they describe an algorithm to find collisions in the MD5
cryptographic hash function. Later, Patrick Stach wrote an efficient
implementation of their algorithm. In this demo, I illustrate how one
can exploit this weakness to make pairs of executable files that have
the same size and MD5 hash, yet behave differently.
- unixcrypt-breaker: break unix "crypt" encryption (2008)
An automated tool for breaking the encryption of the old unix crypt(1)
tool. It can guess substantial portions of the plaintext without
previous knowledge of the key.
- easyrender (2013)
Efficient functions for rendering vector graphics to PDF, PostScript,
- fixedprec (2013)
A reasonably efficient implementation of arbitrary-but-fixed precision
- superdoc (2013)
This package extends Cabal's documentation building capabilities. It
extends the Haddock markup language with syntax for subscripts,
superscripts, bold text, non-breaking spaces, and images.
- newsynth (2013)
An implementation of single-qubit approximate synthesis in the
Clifford+T gate set, based on my paper with Julien Ross, "Optimal
ancilla-free Clifford+T approximation of z-rotations".
- minisat-solver (2016)
High-level Haskell bindings for the well-known MiniSat satisfiability
solver. This can be easily integrated into other programs as an
efficient turn-key solution to many search problems.
Software that I maintain or have contributed to
- Nap: Linux Napster Client (2001)
Nap is a console napster client written by Kevin Sullivan. It runs on
Linux, OpenBSD, and other operating systems. I have been maintaining
it since February 2001.
- Gnut: Linux Gnutella Client (2001)
Gnut is a console-based linux Gnutella client maintained by Robert
Munafo. I made some contributions that haven't yet made it into the
- NUT: Network UPS Tools (2005)
NUT is a set of drivers and tools for Uninterruptible Power Supplies
(UPSs). I have been involved in maintaining the newhidups driver,
which supports USB devices.
- HexGUI: Hex client (2020)
HexGUI is an application to display a Hex game board, keep track of a
game tree (a sequence of moves with variations), add comments to
games, and load and save games in SGF format. It can also attach to a
Hex strategy engine, such as MoHex, to play against the computer or
compute best-play outcomes.
Software to run specific hardware
- Linux and the Belkin Universal UPS (2003)
Belkinunv is a driver for the Belkin Universal UPS (uninterruptible
power supply). This driver is integrated with the existing NUT
(Network UPS Tools) package. I also provide an unofficial description
of the "smart" serial communication protocol used to communicate with
the Belkin Universal UPS.
- Linux and the APC Back-UPS ES (2005)
The APC Back-UPS ES is another UPS (uninterruptible power supply),
connected to a computer via a USB port. I have made a few tweaks to
the NUT (Network UPS Tools) "newhidups" driver to get it to work
smoothly with this UPS.
- Installing Linux on a Fujitsu P2120A LifeBook (2003)
This page describes my experience installing Linux on my Fujitsu
P2120A LifeBook. It includes a description of how to change the
keyboard layout to fix the annoying "right shift key" problem.
- Installing Linux on an IBM Thinkpad X31 (2004)
This page describes my experience installing Linux on an IBM Thinkpad
X31, particularly how to get the built-in wireless adapter to work.
- CUPS wrapper for Lexmark Z32 (2005)
Lexmark makes a binary-only Linux driver for the Z22 and Z32
printers. This page provides software to integrate this driver with
the CUPS printing environment.
- sudoku: create Sudoku puzzles (2006)
This is a command line program for creating high-quality Sudoku
puzzles in Text or HTML format. I wrote this in 2005-2006 when Sudoku
was the craze of the day.
- GLIBC pseudo-random number generator (2007)
The GNU C library's random() function provides pseudo-random
numbers via a linear additive feedback method. A description of the
exact algorithm used is hard to find, so I have documented it here.
- Creating high-quality PDF/A documents using LaTeX (2014)
A PDF/A document is a special kind of PDF document that has been
optimized for long-term archiving. Many organizations, such as
universities, require certain documents, such as Master's and
Ph.D. theses, to be prepared in PDF/A format. This document provides
step-by-step instructions for generating valid PDF/A from LaTeX
- Review of Linux OCR software (2007)
Optical character recognition (OCR) is a difficult and finicky
problem. In the open-source world, there are relatively few choices of
quality OCR software. This document compares three different Linux OCR
programs: Ocrad, GOCR, and Tesseract.
Back to Homepage:
Peter Selinger /
Department of Mathematics and Statistics /
/ PGP key