I write stuff

Coqueries

Anything related to the Coq proof assistant.

• A taxonomy of expression transformations

  1. 0. Introduction
  2. 1. A classification
  3. 2. Expression transformations in Coq
  4. 3. Control mechanisms in Coq
  5. 4. An extension proposal: atomic reductions
• 1. What happens when you run Qed

Misc.

My enlightened ramblings.

• Evaluation strategies

  1. All you ever wanted to know about evaluation strategies (and more)
  2. Call-by-macro vs. call-by-name
  3. Jensen's device
• 1. On impurity (and Haskell)
  2. Notes on a geometric interpretation of the magic square of squares problem