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. [More...]

• 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. [More...]

• 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. [More...]

• PPL - A Prototypical Programming Language (with Ari Lamstein, 2000).
  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. [More...]

• 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. [More...]

• Newsynth - Single-Qubit Approximate Synthesis (2013)
  In our paper "Optimal 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. [More...]

• Skilift - Parallelized product formula circuits for Hamiltonian simulation (2023)
  In our paper "Some improvements to product formula circuits for Hamiltonian simulation", Andre Kornell and I described an algorithm for arranging the circuit for Trotter-based Hamiltonian simulation to make it highly parallel. This Quipper code implements the method of the paper. [More...]

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. [More...]

• 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 space. [More...]

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. [More...]

• hexboard.sty: Macros for Hex (2022)
  A set of LaTeX macros for typesetting Hex boards and positions. [More...]

XML formatting

• 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. [More...]

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 locations. [More...]

• 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. [More...]

• 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 mp3 coder). [More...]

• 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. [More...]

• 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 printing. [More...]

• 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 resolution. [More...]

• 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. [More...]

• 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. [More...]

• 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. [More...]

Haskell packages

• easyrender (2013)
  Efficient functions for rendering vector graphics to PDF, PostScript, and EPS. [More...]

• fixedprec (2013)
  A reasonably efficient implementation of arbitrary-but-fixed precision real numbers. [More...]

• 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. [More...]

• 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". [More...]

• 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. [More...]

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. [More...]

• 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 official release. [More...]

• 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. [More...]

• 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. [More...]

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. [More...]

• 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. [More...]

• 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. [More...]

• 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. [More...]

• 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. [More...]

Entertainment

• 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. [More...]

Documentation

• 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. [More...]

• Introduction to Docker (2022)
  Docker is a useful tool, but for new users, useful information on Docker is hard to find. When I searched the web for introductions to Docker, I found many documents that answer the wrong questions. This is my own attempt at explaining how to use Docker. [More...]

LaTeX resources

• 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 sources. [More...]

• BibTeX style files (2022)
  Some scientific journals have specific instructions for how to format bibliographic references, but do not provide a BibTeX style file for doing so. I provide BibTeX style files for several such journals. [More...]

Software Reviews

• 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. [More...]