A bunch of Haskell source code to go with this paper. The code works with ghc 7.0.2 and ghc 7.0.3 and makes heavy use of functional dependencies in type classes. The goal is to implement the quantum lambda-calculus developed in an MSCS paper written with P. Selinger as an embedded language in Haskell, while keeping the linearity constraints. Ultimately, a QRAM model is simulated using a state monad and the teleportation algorithm is shown to work (in FullQLCMonad.hs). This is a work with Steve Zdancewic.

Incidentally, while working on the project we discovered a bug in the Haskell type checker...

- LocConf, a library to help proving local confluence of rewrite systems (compiles with coq 8.2pl1 and ssreflect 1.2). The documentation is also available online.

- A proof in coq version 8.2, done the hard way (apparently it can be done in a much leaner manner). You can also get the source if you want to compile it

- Macro for easily making trees in latex: [PDF | Latex source]

- An old page with bookmarks (in french).
- Des recettes de cuisine.